Constructive Data Refinement in Typed Lambda Calculus

Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A new treatment of data refinement in typed lambda calculus is proposed, phrased in terms of pre-logical relations [HS99] rather than logical relations, and incorporating a constructive element. Constructive data refinement is shown to have desirable properties, and a substantial example of refinement is presented.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publicationThird International Conference, FOSSACS 2000 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 Berlin, Germany, March 25 – April 2, 2000 Proceedings
EditorsJerzy Tiuryn
PublisherSpringer Berlin Heidelberg
Pages161-176
Number of pages16
ISBN (Electronic)978-3-540-46432-7
ISBN (Print)978-3-540-67257-9
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1784
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Cite this