Lambda calculus and intuitionistic linear logic

DOI10.1023/A:1005092630115zbMATH Open0894.03013OpenAlexW1582221715MaRDI QIDQ1378432FDOQ1378432

Authors: Luca Roversi, Simona Ronchi Della Rocca 

Publication date: 11 February 1998

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005092630115

Recommendations

• Lilac: a functional programming language based on linear logic
• A Parigot-style linear \(\lambda\)-calculus for full intuitionistic linear logic
• Linear lambda-terms and natural deduction
• THE JUDGEMENT CALCULUS FOR INTUITIONISTIC LINEAR LOGIC: PROOF THEORY AND SEMANTICS

zbMATH Keywords

natural deductiontyped lambda calculuscategorical modelCurry-Howard IsomorphismIntuitionistic Linear Logictyped functional languagetyped functional programming

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cited In (24)

• Title not available (Why is that?)
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• New Curry-Howard terms for full linear logic
• Three faces of natural deduction
• Initial algebra semantics for lambda calculi
• A comparison between lambek syntactic calculus and intuitionistic linear propositional logic
• The Intensional Lambda Calculus
• On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic
• Preface
• Semantics of linear/modal lambda calculus
• Characterizing polynomial and exponential complexity classes in elementary lambda-calculus
• Factorization in call-by-name and call-by-value calculi via linear logic
• Lambda terms for natural deduction, sequent calculus and cut elimination
• The bang calculus and the two Girard's translations
• Finite generation and presentation problems for lambda calculus and combinatory logic
• Applications of infinitary lambda calculus
• Nonmodularity results for lambda calculus
• THE JUDGEMENT CALCULUS FOR INTUITIONISTIC LINEAR LOGIC: PROOF THEORY AND SEMANTICS
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Title not available (Why is that?)
• Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
• Resource operators for \(\lambda\)-calculus
• Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
• Thunks and the λ-calculus

This page was built for publication: Lambda calculus and intuitionistic linear logic

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