Resource operators for \(\lambda\)-calculus
From MaRDI portal
Publication:876041
DOI10.1016/j.ic.2006.08.008zbMath1111.68018OpenAlexW2083331063MaRDI QIDQ876041
Stéphane Lengrand, Delia Kesner
Publication date: 16 April 2007
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2006.08.008
Functional programming and lambda calculus (68N18) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Combinatory logic and lambda calculus (03B40)
Related Items
The Prismoid of Resources, On explicit substitution with names, Non-Deterministic Functions as Non-Deterministic Processes (Extended Version), Proof nets and the call-by-value \(\lambda\)-calculus, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, Node Replication: Theory And Practice, Focused linear logic and the \(\lambda\)-calculus, A prismoid framework for languages with resources, The spirit of node replication, Strong Normalisation of Cut-Elimination That Simulates β-Reduction, Intersection Types for the Resource Control Lambda Calculi
Uses Software
Cites Work
- Linear logic
- Computational interpretations of linear logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Explicit substitution. On the edge of strong normalization
- An equivalence between lambda- terms
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Lambda calculus and intuitionistic linear logic
- A general theory of sharing graphs
- Polarized proof-nets and \(\lambda \mu\)-calculus
- Higher order unification via explicit substitutions
- Pattern matching as cut elimination
- Intersection types for explicit substitutions
- Perpetuality in a named lambda calculus with explicit substitutions
- Cut rules and explicit substitutions
- A λ-calculus with explicit weakening and explicit substitution
- Functional back-ends within the lambda-sigma calculus
- λν, a calculus of explicit substitutions which preserves strong normalisation
- Interacting with Modal Logics in the Coq Proof Assistant
- A Terminating and Confluent Linear Lambda Calculus
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Reductions, intersection types, and explicit substitutions
- Linear explicit substitutions
- Proof nets and explicit substitutions
- Explicit substitutions
- Foundations of Software Science and Computation Structures
- A syntax for linear logic
- Automated Deduction – CADE-19
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
