Constructive data refinement in typed lambda calculus

DOI10.1007/3-540-46432-8_11MaRDI QIDQ4508300zbMATH OpenFDO

Authors Furio Honsell, John Longley, Donald Sannella, Andrzej Tarlecki

Publication date 17 January 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46432-8_11

zbMATH Keywords

pre-logical relationstyped lambda calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Data refinement for call-by-value programming languages
• Types and invariants in the refinement calculus
• Axiomatics for data refinement in call by value programming languages
• Data refinement by calculation
• An algebraic formulation for data refinement

Cited in

(4)

• Soundness of data refinement for a higher-order imperative language
• Prelogical relations
• Refinement Types as Proof Irrelevance
• Data refinement for call-by-value programming languages

This page was built for publication: Constructive data refinement in typed lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4508300)