A notation for lambda terms. A generalization of environments

DOI10.1016/S0304-3975(97)00184-9zbMath0901.03015MaRDI QIDQ1129257

Gopalan Nadathur, Debra Sue Wilson

Publication date: 13 August 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

environmentlambda calculuscategory of termsconfluence and noetherianity propertiesexplicit substitution notationslambda terms as representation devices

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ Mechanized metatheory revisited

Uses Software

• Nuprl
• Automath
• LCF
• Elf

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• The categorical abstract machine
• The calculus of constructions
• Church-Rosser theorem for a rewriting system on categorical combinators
• An efficient interpreter for the lambda-calculus
• What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• Edinburgh LCF. A mechanized logic of computation
• Categorical combinators
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A framework for defining logics
• Explicit substitutions
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture