Refinement Types as Proof Irrelevance

DOI10.1007/978-3-642-02273-9_13MaRDI QIDQ3637193zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Refinement types for logical frameworks and their interpretation as proof irrelevance
• Principles and applications of refinement types
• A bidirectional refinement type system for LF
• Publication:4508300
• scientific article; zbMATH DE number 1301735

Cites work

• A bidirectional refinement type system for LF
• A framework for defining logics
• Inheritance as implicit coercion
• Intersection-types à la Church
• Propositions as [Types]
• Tridirectional typechecking
• Types for Proofs and Programs

Cited in

(3)

• Refinement types for logical frameworks and their interpretation as proof irrelevance
• Formalising foundations of mathematics
• Representing model theory in a type-theoretical logical framework

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Refinement Types as Proof Irrelevance

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