A notation for lambda terms. A generalization of environments
From MaRDI portal
Publication:1129257
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)
environmentlambda calculuscategory of termsconfluence and noetherianity propertiesexplicit substitution notationslambda terms as representation devices
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
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