Monadic translation of classical sequent calculus

DOI10.1017/S0960129512000436MaRDI QIDQ5410235zbMATH OpenFDO

Authors José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto

Publication date 16 April 2014

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

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Functional programming and lambda calculus (68N18)

Recommendations

• Monadic Translation of Intuitionistic Sequent Calculus
• Translations from natural deduction to sequent calculus
• scientific article; zbMATH DE number 2119475
• Computational Semantics for Monadic Quantifiers
• Transforming functional logic programs into monadic functional programs
• The monadic hybrid calculus
• On monadic theories of monadic predicates
• Monadic second-order logic on finite sequences
• On the monadic second-order transduction hierarchy
• On the relations between monadic semantics

Cites work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-Value  -calculus and LJQ
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
• Domain-free pure type systems
• Monadic Translation of Intuitionistic Sequent Calculus
• Notions of computation and monads
• Proofs of strong normalisation for second order classical natural deduction
• Soundness and principal contexts for a shallow polymorphic type system based on classical logic
• Strong normalization proof with CPS-translation for second order classical natural deduction
• Strong normalization proofs by CPS-translations
• The duality of computation under focus
• Weak normalization implies strong normalization in a class of non-dependent pure type systems

Cited in

(7)

• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• Monadic Translation of Intuitionistic Sequent Calculus
• scientific article; zbMATH DE number 1948182 (Why is no real title available?)
• scientific article; zbMATH DE number 1956457 (Why is no real title available?)
• scientific article; zbMATH DE number 2003163 (Why is no real title available?)
• Confluence for classical logic through the distinction between values and computations
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

This page was built for publication: Monadic translation of classical sequent calculus

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