Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus

DOI10.1007/978-3-642-14203-1_1MaRDI QIDQ5747746zbMATH OpenOpenAlexFDO

Authors Anders Schack-Nielsen, Carsten Schürmann

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_1

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Simultaneous substitution in the typed lambda calculus
• Formalization of a λ-calculus with explicit substitutions in Coq
• A \(\lambda\)-calculus with explicit weakening and explicit substitution
• scientific article; zbMATH DE number 1088029
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• A linearization of the Lambda-calculus and consequences
• Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• The \(\lambda\)-context calculus

Cites work

• scientific article; zbMATH DE number 1670733 (Why is no real title available?)
• scientific article; zbMATH DE number 2185670 (Why is no real title available?)
• A notation for lambda terms. A generalization of environments
• Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Explicit substitutions
• FreshML: programming with binders made simple
• Linear explicit substitutions
• Practical Programming with Higher-Order Encodings and Dependent Types
• The Abella Interactive Theorem Prover (System Description)
• The Theory of Calculi with Explicit Substitutions Revisited

Cited in

(7)

• \textsc{Lincx}: a linear logical framework with first-class contexts
• A Linear Spine Calculus
• Linear explicit substitutions
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• scientific article; zbMATH DE number 1088029 (Why is no real title available?)
• Linear lambda calculus and deep inference
• Formalization of a λ-calculus with explicit substitutions in Coq

Describes a project that uses

Uses Software

• Abella
• Bedwyr
• FreshML
• Twelf
• HOL

This page was built for publication: Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747746)