External and internal syntax of the \(\lambda \)-calculus

DOI10.1016/j.jsc.2010.01.010zbMath1192.68140OpenAlexW2033368611MaRDI QIDQ968531

Masahiko Sato, Randy Pollack

Publication date: 5 May 2010

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2010.01.010

zbMATH Keywords

lambda calculusformal proofbinding

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (6)

A unified treatment of syntax with binders ⋮ A canonical locally named representation of binding ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle ⋮ Viewing \({\lambda}\)-terms through maps ⋮ Term-generic logic ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Uses Software

• Isabelle/HOL
• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Theory of symbolic expressions. II
• Substitution revisited
• Untersuchungen über das logische Schliessen. II
• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• A canonical locally named representation of binding
• Engineering formal metatheory
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Alpha-structural recursion and induction
• Barendregt’s Variable Convention in Rule Inductions
• A framework for defining logics
• Automating inversion of inductive predicates in Coq

This page was built for publication: External and internal syntax of the \(\lambda \)-calculus