Resource operators for -calculus

DOI10.1016/J.IC.2006.08.008zbMATH Open1111.68018OpenAlexW2083331063MaRDI QIDQ876041FDOQ876041

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

Recommendations

• Term Rewriting and Applications
• scientific article; zbMATH DE number 1086680
• Intuitionistic differential nets and lambda-calculus
• Proof nets and the linear substitution calculus
• Geometry of resource interaction -- \textit{a minimalist approach}

zbMATH Keywords

term calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Computational interpretations of linear logic
• Title not available (Why is that?)
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• An equivalence between lambda- terms
• Polarized proof-nets and \(\lambda \mu\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Explicit substitutions
• Title not available (Why is that?)
• Automated Deduction – CADE-19
• A general theory of sharing graphs
• A Terminating and Confluent Linear Lambda Calculus
• A \(\lambda\)-calculus with explicit weakening and explicit substitution
• Title not available (Why is that?)
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Proof nets and explicit substitutions
• Title not available (Why is that?)
• Interacting with Modal Logics in the Coq Proof Assistant
• Reductions, intersection types, and explicit substitutions
• Foundations of Software Science and Computation Structures
• Higher order unification via explicit substitutions
• Explicit substitution. On the edge of strong normalization
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Lambda calculus and intuitionistic linear logic
• Pattern matching as cut elimination
• Intersection types for explicit substitutions
• Perpetuality in a named lambda calculus with explicit substitutions
• Cut rules and explicit substitutions
• Title not available (Why is that?)
• Functional back-ends within the lambda-sigma calculus
• Title not available (Why is that?)
• Linear explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A syntax for linear logic

Cited In (14)

• Focused linear logic and the \(\lambda\)-calculus
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• The spirit of node replication
• The Prismoid of Resources
• Term Rewriting and Applications
• Node Replication: Theory And Practice
• Proof nets and the call-by-value \(\lambda\)-calculus
• On explicit substitution with names
• Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)
• Storage operators and directed lambda-calculus
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Intersection Types for the Resource Control Lambda Calculi
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• A prismoid framework for languages with resources

Uses Software

• Coq

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

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