Normalization for the Simply-Typed Lambda-Calculus in Twelf
From MaRDI portal
Publication:2871835
DOI10.1016/j.entcs.2007.11.009zbMath1278.68245OpenAlexW2152365225MaRDI QIDQ2871835
Publication date: 10 January 2014
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2007.11.009
Related Items
A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ POPLMark reloaded: Mechanizing proofs by logical relations
Uses Software
Cites Work
- Perpetual reductions in \(\lambda\)-calculus
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Towards a mechanized metatheory of standard ML
- A Coverage Checking Algorithm for LF
- A framework for defining logics
- On equivalence and canonical forms in the LF type theory
- Types for Proofs and Programs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
