Computation with classical sequents

DOI10.1017/S0960129508006762MaRDI QIDQ3520146zbMATHOpenAlexFDO

Authors Steffen Van Bakel, Pierre Lescanne

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

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

Recommendations

• Theoretical Computer Science
• Programming Languages and Systems
• scientific article; zbMATH DE number 1231511
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• On semantics of a term calculus for classical logic

Cites work

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

Cited in

(8)

• On the computational representation of classical logical connectives
• Sequent calculus as a compiler intermediate language
• Theoretical Computer Science
• Programming Languages and Systems
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Sequential operators in computability logic
• Semantic types and approximation for Featherweight Java
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types

This page was built for publication: Computation with classical sequents

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