Viewing \({\lambda}\)-terms through maps

DOI10.1016/J.INDAG.2013.08.003zbMath1359.03016OpenAlexW2201091269MaRDI QIDQ740485

Randy Pollack, Helmut Schwichtenberg, Takafumi Sakurai, Masahiko Sato

Publication date: 3 September 2014

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.indag.2013.08.003

zbMATH Keywords

lambda calculusnominal logicformal proofbindingde Bruijnmachine checked proofnameless dummies

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Unnamed Item ⋮ Alpha-structural induction and recursion for the lambda calculus in constructive type theory ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus

Uses Software

• Isabelle/HOL
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Theory of symbolic expressions. I
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Nominal techniques in Isabelle/HOL
• External and internal syntax of the \(\lambda \)-calculus
• Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• Engineering formal metatheory
• Inductive-Inductive Definitions
• A mechanical proof of the Church-Rosser theorem
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Computer Science Logic
• Context rewriting

This page was built for publication: Viewing \({\lambda}\)-terms through maps