Refinement Types as Proof Irrelevance

DOI10.1007/978-3-642-02273-9_13zbMath1202.68107OpenAlexW1532507833MaRDI QIDQ3637193

William Lovas, Frank Pfenning

Publication date: 7 July 2009

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

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_13

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Representing model theory in a type-theoretical logical framework, Formalising foundations of mathematics

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Inheritance as implicit coercion
• Intersection-types à la Church
• Tridirectional typechecking
• A framework for defining logics
• Propositions as [Types]
• Types for Proofs and Programs