On equivalence and canonical forms in the LF type theory
From MaRDI portal
Publication:5277716
DOI10.1145/1042038.1042041zbMATH Open1367.03055arXivcs/0110028OpenAlexW2043740265MaRDI QIDQ5277716FDOQ5277716
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Abstract: Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent, strongly-normalizing notion of reduction. Coquand has considered a different approach, directly proving the correctness of a practical equivalance algorithm based on the shape of terms. Neither approach appears to scale well to richer languages with unit types or subtyping, and neither directly addresses the problem of conversion to canonical. In this paper we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages, and yields a new notion of canonical form sufficient for adequate encodings of logical systems. The algorithm is proved complete by a Kripke-style logical relations argument similar to that suggested by Coquand. Crucially, both the algorithm itself and the logical relations rely only on the shapes of types, ignoring dependencies on terms.
Full work available at URL: https://arxiv.org/abs/cs/0110028
Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
Cited In (18)
- Automated techniques for provably safe mobile code.
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mechanizing metatheory in a logical framework
- Redundancy elimination for LF
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
- POPLMark reloaded: Mechanizing proofs by logical relations
- Mechanizing proofs with logical relations β Kripke-style
- Hybridizing a logical framework
- Polarised subtyping for sized types
- Title not available (Why is that?)
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
- Ξ±Check: A mechanized metatheory model checker
- Structural recursion with locally scoped names
- Normalization by evaluation for modal dependent type theory
- Title not available (Why is that?)
- Parametricity, type equality, and higher-order polymorphism
- A logical framework with higher-order rational (circular) terms
- Normalization for the simply-typed lambda-calculus in Twelf
Uses Software
Recommendations
- Title not available (Why is that?) π π
- Title not available (Why is that?) π π
- Type theories, normal forms, and \(D_{\infty}\)-lambda-models π π
- On the equivalence of types π π
- Equational theories for inductive types π π
- Equivalences between logics and their representing type theories π π
- Canonicity for 2-dimensional type theory π π
- Canonicity for cubical type theory π π
- Automated Deduction β CADE-20 π π
- Canonicity and homotopy canonicity for cubical type theory π π
This page was built for publication: On equivalence and canonical forms in the LF type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277716)
