On equivalence and canonical forms in the LF type theory
From MaRDI portal
Publication:5277716
DOI10.1145/1042038.1042041zbMath1367.03055arXivcs/0110028OpenAlexW2043740265MaRDI QIDQ5277716
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
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
This page was built for publication: On equivalence and canonical forms in the LF type theory
