A notation for lambda terms. A generalization of environments
type: Item
instance of: scholarly article
title: A notation for lambda terms. A generalization of environments
zbMATH Open document ID: 0901.03015
DOI: 10.1016/S0304-3975(97)00184-9
author: Gopalan Nadathur
author: Debra Sue Wilson
published in: Theoretical Computer Science
publication date: 1998-08-13T00:00:00Z
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 1190297
zbMATH Keywords: lambda calculus
zbMATH Keywords: lambda terms as representation devices
zbMATH Keywords: explicit substitution notations
zbMATH Keywords: confluence and noetherianity properties
zbMATH Keywords: category of terms
zbMATH Keywords: environment
describes a project that uses: Nuprl
describes a project that uses: LCF
describes a project that uses: Elf
describes a project that uses: Automath
MaRDI profile type: Publication
cites work: Explicit substitutions
cites work: An efficient interpreter for the lambda-calculus
cites work: Q5667469
cites work: Q4175528
cites work: The calculus of constructions
cites work: The categorical abstract machine
cites work: Categorical combinators
cites work: Q3785893
cites work: Orderings for term-rewriting systems
cites work: What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q5726943
cites work: Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
cites work: A framework for defining logics
cites work: Q5686017
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Proving and applying program transformations expressed with second-order patterns
cites work: Q3918095
cites work: Q5581665
cites work: Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
cites work: Q4189277
cites work: Q4259974
cites work: Q5687569
cites work: Q3204068
cites work: Church-Rosser theorem for a rewriting system on categorical combinators
Recommended article: Q4259974
Recommended article: An environment machine for the λμ-calculus
Recommended article: A useful \(\lambda\)-notation
Recommended article: A generalization of the lambda algebra
Recommended article: An equivalence between lambda- terms
Recommended article: A calculus of lambda calculus contexts
Recommended article: The \(\lambda\)-context calculus
Recommended article: Q4474832
Recommended article: Lambda terms for natural deduction, sequent calculus and cut elimination
Recommended article: Lambda terms definable as combinators
description: scientific article; zbMATH DE number 1190297