Viewing \({\lambda}\)-terms through maps
type: Item
instance of: scholarly article
title: Viewing \({\lambda}\)-terms through maps
zbMATH Open document ID: 1359.03016
author: Masahiko Sato
author: Randy Pollack
author: Helmut Schwichtenberg
author: Takafumi Sakurai
published in: Indagationes Mathematicae. New Series
publication date: 2014-09-03T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6339334
zbMATH Keywords: binding
zbMATH Keywords: de Bruijn
zbMATH Keywords: nameless dummies
zbMATH Keywords: lambda calculus
zbMATH Keywords: nominal logic
zbMATH Keywords: formal proof
zbMATH Keywords: machine checked proof
describes a project that uses: Isabelle/HOL
describes a project that uses: Nominal Isabelle
MaRDI profile type: Publication
full work available at URL: j.indag.2013.08.003
OpenAlex ID: W2201091269
cites work: Engineering formal metatheory
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q5565097
cites work: Q5667469
cites work: A general formulation of simultaneous inductive-recursive definitions in type theory
cites work: Inductive-Inductive Definitions
cites work: A new approach to abstract syntax with variable binding
cites work: Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
cites work: Context rewriting
cites work: Some lambda calculus and type theory formalized
cites work: Nominal logic, a first order theory of names and binding
cites work: Theory of symbolic expressions. I
cites work: Q4016562
cites work: External and internal syntax of the \(\lambda \)-calculus
cites work: Computer Science Logic
cites work: A mechanical proof of the Church-Rosser theorem
cites work: Nominal techniques in Isabelle/HOL
DOI: 10.1016/J.INDAG.2013.08.003
description: scientific article; zbMATH DE number 6339334