Constructive Data Refinement in Typed Lambda Calculus

13 years 8 months ago

Download homepages.inf.ed.ac.uk

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.

Furio Honsell, John Longley, Donald Sannella, Andr

Real-time Traffic

Constructive Data Refinement | Data Refinement | FOSSACS 2000 | Software Engineering | Typed Lambda Calculus |

claim paper

» Lambda Types on the Lambda Calculus with Abbreviations

» Step Indexed Realizability Semantics for a CallbyValue Language Based on Basic Combinatori...

» A Modal Lambda Calculus with Iteration and Case Constructs

» A typed lambda calculus with intersection types

» Embedding Pure Type Systems in the LambdaPiCalculus Modulo

» Inductive Coinductive and Pointed Types

» A Computational Treatment of Korean Temporal Markers OE and DONGAN

» Propositions as sessions

Post Info
More Details (n/a)

Added	24 Aug 2010
Updated	24 Aug 2010
Type	Conference
Year	2000
Where	FOSSACS
Authors	Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki

Comments (0)

Sciweavers

Constructive Data Refinement in Typed Lambda Calculus

Constructive Data Refinement | Data Refinement | FOSSACS 2000 | Software Engineering | Typed Lambda Calculus |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers