Monadic translation of classical sequent calculus
From MaRDI portal
Publication:5410235
DOI10.1017/S0960129512000436zbMath1311.68042MaRDI QIDQ5410235
Luís Pinto, José Espírito Santo, Koji Nakazawa, Ralph Matthes
Publication date: 16 April 2014
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)
Cites Work
- Notions of computation and monads
- Strong normalization proofs by CPS-translations
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Completeness of continuation models for \(\lambda_\mu\)-calculus
- Soundness and principal contexts for a shallow polymorphic type system based on classical logic
- The Duality of Computation under Focus
- Monadic Translation of Intuitionistic Sequent Calculus
- Proofs of strong normalisation for second order classical natural deduction
- Strong normalization proof with CPS-translation for second order classical natural deduction
- Domain-free pure type systems
- Call-by-Value -calculus and LJQ
- Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
- Weak normalization implies strong normalization in a class of non-dependent pure type systems
This page was built for publication: Monadic translation of classical sequent calculus
