External and internal syntax of the \(\lambda \)-calculus
type: Item
instance of: scholarly article
title: External and internal syntax of the \(\lambda \)-calculus
zbMATH Open document ID: 1192.68140
author: Masahiko Sato
author: Randy Pollack
published in: Journal of Symbolic Computation
publication date: 2010-05-05T00:00:00Z
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 5704034
zbMATH Keywords: binding
zbMATH Keywords: lambda calculus
zbMATH Keywords: formal proof
describes a project that uses: Nominal Isabelle
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
full work available at URL: j.jsc.2010.01.010
OpenAlex ID: W2033368611
cites work: Engineering formal metatheory
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q5565097
cites work: Automating inversion of inductive predicates in Coq
cites work: Q5565113
cites work: Q5667469
cites work: A new approach to abstract syntax with variable binding
cites work: Untersuchungen über das logische Schliessen. II
cites work: A framework for defining logics
cites work: Recursive functions of symbolic expressions and their computation by machine, Part I
cites work: Q5601829
cites work: Q4281480
cites work: Some lambda calculus and type theory formalized
cites work: Q3999860
cites work: Nominal logic, a first order theory of names and binding
cites work: Alpha-structural recursion and induction
cites work: A canonical locally named representation of binding
cites work: Q5807658
cites work: Theory of symbolic expressions. I
cites work: Theory of symbolic expressions. II
cites work: Q4016562
cites work: Q3044486
cites work: Substitution revisited
cites work: Q5610986
cites work: Nominal techniques in Isabelle/HOL
cites work: Barendregt’s Variable Convention in Rule Inductions
DOI: 10.1016/J.JSC.2010.01.010
description: scientific article; zbMATH DE number 5704034