Strong Normalization of the Dual Classical Sequent Calculus

DOI10.1007/11591191_13MaRDI QIDQ5387838zbMATH OpenOpenAlexFDO

Authors Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2318/28867

Mathematics Subject Classification ID

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

Recommendations

• Investigations on the dual calculus
• A strong normalization result for classical logic
• Arithmetical proofs of strong normalization results for symmetric lambda calculi
• scientific article; zbMATH DE number 2080223
• A short proof of the strong normalization of classical natural deduction with disjunction

Cited in

(11)

• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• Investigations on the dual calculus
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• A sequent calculus with dependent types for classical arithmetic
• scientific article; zbMATH DE number 4195935 (Why is no real title available?)
• Curry-Howard for sequent calculus at last!
• Classical Logic with Mendler Induction
• scientific article; zbMATH DE number 2247256 (Why is no real title available?)
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication: Strong Normalization of the Dual Classical Sequent Calculus

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