The locally nameless representation
From MaRDI portal
Publication:1945914
DOI10.1007/s10817-011-9225-2zbMath1260.68368OpenAlexW2091657052MaRDI QIDQ1945914
Publication date: 17 April 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9225-2
Related Items
Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ The Role of Indirections in Lazy Natural Semantics ⋮ Composition-nominative logics as institutions ⋮ HOCore in Coq ⋮ Finitary type theories with and without contexts ⋮ Constraint handling rules with binders, patterns and generic quantification ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ A strong call-by-need calculus ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ An extensible equality checking algorithm for dependent type theories ⋮ Higher-Order Modal Logics: Automation and Applications ⋮ Psi-calculi in Isabelle ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Alpha-structural induction and recursion for the lambda calculus in constructive type theory ⋮ Syntactic soundness proof of a type-and-capability system with hidden state ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus ⋮ An extensible approach to session polymorphism ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Nominal techniques in Isabelle/HOL
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Isabelle/HOL. A proof assistant for higher-order logic
- Some lambda calculus and type theory formalized
- Engineering formal metatheory
- Formalizing Soundness of Contextual Effects
- Uniqueness Typing Redefined
- The Zipper
- Natural deduction as higher-order resolution
- F-ing modules
- AURA
- FreshML
- Theorem Proving in Higher Order Logics
