A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
From MaRDI portal
Publication:1850959
DOI10.1023/A:1019964114625zbMath1041.68016OpenAlexW1566183855MaRDI QIDQ1850959
Publication date: 15 December 2002
Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1019964114625
Related Items
Strongly typed term representations in Coq, Kripke models for classical logic, A henkin-style completeness proof for the modal logic S5, Representing model theory in a type-theoretical logical framework, Big-step normalisation, Type-level Computation Using Narrowing in Ωmega, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
Uses Software
