The locally nameless representation

DOI10.1007/S10817-011-9225-2zbMath1260.68368OpenAlexW2091657052MaRDI QIDQ1945914

Arthur Charguéraud

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

zbMATH Keywords

formal proofsbindersmetatheorycofinite quantificationlocally nameless

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (25)

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

• Coq
• ML
• Isabelle/HOL
• Freshml
• LEGO
• PoplMark
• AURA
• Nominal Isabelle

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

This page was built for publication: The locally nameless representation