Resource operators for \(\lambda\)-calculus

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

zbMATH Keywords

term calculus

Mathematics Subject Classification ID

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 (11)

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

• Coq

Cites Work

• 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
• 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

This page was built for publication: Resource operators for \(\lambda\)-calculus