Constructive Data Refinement in Typed Lambda Calculus

Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki

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


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
Number of pages16
ISBN (Electronic)978-3-540-46432-7
ISBN (Print)978-3-540-67257-9
Publication statusPublished - 2000

Publication series

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

Cite this