research-article

A sequent calculus with dependent types for classical arithmetic

Author:

Étienne MiqueyAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 720 - 729

https://doi.org/10.1145/3209108.3209199

Published: 09 July 2018 Publication History

Abstract

In a recent paper [11], Herbelin developed dPAω, a calculus 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 types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type N→A into streams (a0, a1, ...)) and of lazy evaluation with sharing (for these coinductive objects).

Elaborating on previous works, we introduce in this paper a variant of dPAω presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability that we developed to prove the normalization of classical call-by-need [20]. On the other hand, we benefit from dLtp, a classical sequent calculus with dependent types in which type safety is ensured by using delimited continuations together with a syntactic restriction [19]. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness.

References

[1]

Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin. Classical call-by-need sequent calculi: The unity of semantic artifacts. In FLOPS 2012, Proceedings.

Digital Library

[2]

S. Berardi, M. Bezem, and T. Coquand. On the computational content of the axiom of choice. J. Symb. Log., 63(2):600--622, 1998.

[3]

U. Berger. A computational interpretation of open induction. In LICS 2004, Proceedings, page 326, 2004.

Digital Library

[4]

V. Blot. An interpretation of system F through bar recursion. In LICS 2017, Proceedings, pages 1--12, 2017.

[5]

L. Cohen, V. Rahli, M. Bickford, and R. L. Constable. Computability beyond church-turing using choice sequences. In LICS 2018, Proceedings, 2018.

Digital Library

[6]

P.-L. Curien and H. Herbelin. The duality of computation. In ICFP 2000, Proceedings, SIGPLAN Notices 35(9), 2000.

Digital Library

[7]

O. Danvy, K. Millikin, J. Munk, and I. Zerny. Defunctionalized interpreters for call-by-need evaluation. In FLOPS 2010, Proceedings, 2010.

Digital Library

[8]

P. Downen, L. Maurer, Z. M. Ariola, and S. P. Jones. Sequent calculus as a compiler intermediate language. In ICFP 2016, Proceedings, 2016.

Digital Library

[9]

M. H. Escardó and P. Oliva. Bar recursion and products of selection functions. CoRR, abs/1407.7046, 2014. URL: http://arxiv.org/abs/1407.7046.

[10]

H. Herbelin. On the degeneracy of sigma-types in presence of computational classical logic. In TLCA 2005, Proceedings, 2005.

Digital Library

[11]

H. Herbelin. A constructive proof of dependent choice, compatible with classical logic. In LICS 2012, Proceedings, 2012.

Digital Library

[12]

A. Kolmogoroff. Zur deutung der intuitionistischen logik. Mathematische Zeitschrift, 35(1):58--65, Dec 1932.

[13]

J.-L. Krivine. Dependent choice, 'quote' and the clock. Th. Comp. Sc., 308, 2003.

Digital Library

[14]

J.-L. Krivine. Realizability in classical logic. In interactive models of computation and program behaviour. Panoramas et synthèses, 27, 2009.

[15]

J.-L. Krivine. Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis. In CSL 2016, Proceedings, 2016.

[16]

R. Lepigre. A classical realizability model for a semantical value restriction. In ESOP 2016, Proceedings, 2016.

Digital Library

[17]

P. Martin-Löf. An intuitionistic theory of types. In twenty-five years of constructive type theory. Oxford Logic Guides, 36:127--172, 1998.

[18]

É. Miquey. Classical realizability and side-effects. Theses, Univ.é Paris Diderot; Univ. de la República, Uruguay, Nov. 2017. URL: https://hal.inria.fr/tel-01653733.

[19]

É. Miquey. A classical sequent calculus with dependent types. In H. Yang, editor, ESOP 2017, Proceedings, 2017.

Digital Library

[20]

É. Miquey and H. Herbelin. Realizability interpretation and normalization of typed call-by-need λ-calculus with control. In FoSSaCS, Proceedings, 2018.

[21]

G. Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Univ. Paris Diderot, 2013.

[22]

G. Munch-Maccagnoni and G. Scherer. Polarised Intermediate Representation of Lambda Calculus with Sums. In LICS 2015, Proceedings, 2015.

Digital Library

[23]

S. G. Simpson. Subsystems of Second Order Arithmetic. Perspectives in Logic. Cambridge University Press, 2 edition, 2009.

[24]

C. Spector. Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics. 1962.

[25]

P. Wadler. Call-by-value is dual to call-by-name. In ICFP 2003, Proceedings, 2003.

Digital Library

Cited By

Cohen LMiquey ÉTate RGorla D(2021)Evidenced framesProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470514(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470514
Miquey É(2019)A Classical Sequent Calculus with Dependent TypesACM Transactions on Programming Languages and Systems10.1145/323062541:2(1-47)Online publication date: 15-Mar-2019
https://dl.acm.org/doi/10.1145/3230625
Bickford MCohen LConstable RRahli V(2018)Computability Beyond Church-Turing via Choice SequencesProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209200(245-254)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209200

Recommendations

A Classical Sequent Calculus with Dependent Types
Special Issue on ESOP 2017 and Regular Papers

Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well known that this correspondence can be extended to classical logic by enriching the language of proofs with control operators. However, they are ...
Non-classical Elegance for Sequent Calculus Enthusiasts

In this paper we develop what we can describe as a "dual two-sided" cut-free sequent calculus system for the non-classical logics of truth lp, k 3, stt and a non-reflexive logic ts which is, arguably, more elegant than the three-sided sequent calculus ...
Sequent calculus for classical logic probabilized
Abstract
Gentzen’s approach to deductive systems, and Carnap’s and Popper’s treatment of probability in logic were two fruitful ideas that appeared in logic of the mid-twentieth century. By combining these two concepts, the notion of sentence probability, ... $_{}^{}$ $_{}_{_{}}^{_{}}_{}$ $_{}^{}$

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
99
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)1

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cohen LMiquey ÉTate RGorla D(2021)Evidenced framesProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470514(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470514
Miquey É(2019)A Classical Sequent Calculus with Dependent TypesACM Transactions on Programming Languages and Systems10.1145/323062541:2(1-47)Online publication date: 15-Mar-2019
https://dl.acm.org/doi/10.1145/3230625
Bickford MCohen LConstable RRahli V(2018)Computability Beyond Church-Turing via Choice SequencesProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209200(245-254)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209200

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten