Choices in representation and reduction strategies for lambda terms in intensional contexts

DOI10.1007/S10817-004-6885-1MaRDI QIDQ861365zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

implementationlambda calculusexplicit substitutionlambda conversion

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

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

Cites work

• scientific article; zbMATH DE number 1332647 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A \(\lambda\)-calculus with explicit weakening and explicit substitution
• A compiled implementation of strong reduction
• A framework for defining logics
• A notation for lambda terms. A generalization of environments
• A unification algorithm for typed -calculus
• An efficient interpreter for the lambda-calculus
• Closed reduction: explicit substitutions without $\alpha$ -conversion
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Higher order unification via explicit substitutions
• Isabelle/HOL. A proof assistant for higher-order logic
• The calculus of constructions
• Unification under a mixed prefix
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(7)

• Intensional computation with higher-order functions
• scientific article; zbMATH DE number 2090073 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• Teyjus
• Automath
• Twelf
• Nuprl
• Prolog
• Isabelle/HOL
• Coq

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)