A sequent calculus with dependent types for classical arithmetic

DOI10.1145/3209108.3209199zbMATH Open1453.03010arXiv1805.09542OpenAlexW2786132250MaRDI QIDQ5145348FDOQ5145348

Authors: Étienne Miquey 

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: In a recent paper, Herbelin developed a calculus dPA${}^{o}mega$ in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type $NightarrowA$ into streams $(a_0,a_1,ldots)$) and of lazy evaluation with sharing (for these coinductive objects).Building on previous works, we introduce in this paper a variant of dPA${}^{o}mega$ presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dL, a classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation {`a} la Krivine of our calculus that allows us to prove normalization and soundness.

Full work available at URL: https://arxiv.org/abs/1805.09542

Recommendations

• A classical sequent calculus with dependent types
• Realizability interpretation and normalization of typed call-by-need \(\lambda\)-calculus with control
• Dependent choice, `quote' and the clock
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• Strong Normalization of the Dual Classical Sequent Calculus

zbMATH Keywords

dependent typessequent calculusclassical realizabilitydependent choiceclassical arithmeticside effectsCurry-Howard

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) First-order arithmetic and fragments (03F30)

Cited In (1)

• The effects of effects on constructivism

This page was built for publication: A sequent calculus with dependent types for classical arithmetic

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