On equivalence and canonical forms in the LF type theory

DOI10.1145/1042038.1042041zbMath1367.03055arXivcs/0110028OpenAlexW2043740265MaRDI QIDQ5277716

Robert Harper, Frank Pfenning

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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

zbMATH Keywords

type theorylogical frameworks

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (18)

Mechanizing metatheory in a logical framework ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Normalization by evaluation for modal dependent type theory ⋮ αCheck: A mechanized metatheory model checker ⋮ A logical framework with higher-order rational (circular) terms ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ Polarised subtyping for sized types ⋮ Parametricity, type equality, and higher-order polymorphism ⋮ Structural recursion with locally scoped names ⋮ Unnamed Item ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Automated techniques for provably safe mobile code. ⋮ Hybridizing a Logical Framework ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf ⋮ Redundancy Elimination for LF ⋮ \texttt{slepice}: towards a verified implementation of type theory in type theory

Uses Software

• Twelf

This page was built for publication: On equivalence and canonical forms in the LF type theory