Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
From MaRDI portal
Publication:5747746
DOI10.1007/978-3-642-14203-1_1zbMATH Open1291.03022OpenAlexW1759101439MaRDI QIDQ5747746FDOQ5747746
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
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
- The Abella Interactive Theorem Prover (System Description)
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- Practical Programming with Higher-Order Encodings and Dependent Types
- FreshML: programming with binders made simple
- Explicit substitutions
- Title not available (Why is that?)
- The Theory of Calculi with Explicit Substitutions Revisited
- A notation for lambda terms. A generalization of environments
- Linear explicit substitutions
- Title not available (Why is that?)
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
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
- Title not available (Why is that?)
- Linear lambda calculus and deep inference
- Formalization of a λ-calculus with explicit substitutions in Coq
Uses Software
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)
