Choices in representation and reduction strategies for lambda terms in intensional contexts
DOI10.1007/S10817-004-6885-1zbMATH Open1102.68019OpenAlexW2092768924MaRDI QIDQ861365FDOQ861365
Authors: Chuck Liang, Gopalan Nadathur, Xiaochu Qi 
Publication date: 29 January 2007
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-004-6885-1
Recommendations
- scientific article; zbMATH DE number 2090073
- scientific article; zbMATH DE number 1332647
- Processing underspecified semantic representations in the constraint language for lambda structures
- Logical Aspects of Computational Linguistics
- Lambda terms for natural deduction, sequent calculus and cut elimination
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
- scientific article; zbMATH DE number 4045104
- scientific article; zbMATH DE number 3296225
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)
Cites Work
- Isabelle/HOL. A proof assistant for higher-order logic
- A framework for defining logics
- Title not available (Why is that?)
- The calculus of constructions
- Unification under a mixed prefix
- Explicit substitutions
- A unification algorithm for typed \(\overline\lambda\)-calculus
- A \(\lambda\)-calculus with explicit weakening and explicit substitution
- λν, a calculus of explicit substitutions which preserves strong normalisation
- Closed reduction: explicit substitutions without $\alpha$ -conversion
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Higher order unification via explicit substitutions
- A notation for lambda terms. A generalization of environments
- An efficient interpreter for the lambda-calculus
- A compiled implementation of strong reduction
- Title not available (Why is that?)
- Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
Cited In (7)
- Intensional computation with higher-order functions
- Title not available (Why is that?)
- Mechanized metatheory revisited
- A \(\rho\)-calculus of explicit constraint application
- Logical Aspects of Computational Linguistics
- SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
Uses Software
This page was built for publication: Choices in representation and reduction strategies for lambda terms in intensional contexts
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q861365)
