Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance

DOI10.2168/LMCS-6(4:5)2010zbMath1202.68108arXiv1009.1861MaRDI QIDQ3064169

William Lovas, Frank Pfenning

Publication date: 20 December 2010

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1009.1861

zbMATH Keywords

logical frameworksrefinement typesproof irrelevance

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 (1)

Extensible Datasort Refinements

Uses Software

• Nuprl
• Delphin
• Forsythe

This page was built for publication: Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance