Computation with classical sequents

DOI10.1017/S0960129508006762zbMath1173.03011OpenAlexW2027556526MaRDI QIDQ3520146

Pierre Lescanne, Steffen van Bakel

Publication date: 15 August 2008

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129508006762

zbMATH Keywords

lambda calculusreduction ruleapplication formal language

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (3)

A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types ⋮ Semantic types and approximation for Featherweight Java ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)

Cites Work

• Unnamed Item
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The system \({\mathcal F}\) of variable types, fifteen years later
• Classical logic, storage operators and second-order lambda-calculus
• Untersuchungen über das logische Schliessen. I
• Intersection types for explicit substitutions
• A symmetric lambda calculus for classical program extraction
• A new deconstructive logic: linear logic
• Lambda terms for natural deduction, sequent calculus and cut elimination
• A formulation of the simple theory of types

This page was built for publication: Computation with classical sequents