Document Open Access Logo

A Stratified Approach to Löb Induction

Authors Daniel Gratzer , Lars Birkedal

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.23.pdf
  • Filesize: 0.94 MB
  • 22 pages

Document Identifiers

Author Details

Daniel Gratzer
  • Aarhus University, Denmark
Lars Birkedal
  • Aarhus University, Denmark

Funding

Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.

Cite As Get BibTex

Daniel Gratzer and Lars Birkedal. A Stratified Approach to Löb Induction. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 23:1-23:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.23

Abstract

Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories.
Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Denotational semantics
  • Theory of computation → Modal and temporal logics
Keywords
  • Dependent type theory
  • guarded recursion
  • modal type theory
  • canonicity
  • categorical gluing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Robert Atkey and Conor McBride. Productive Coprogramming with Guarded Recursion. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP ’13, pages 197-208. Association for Computing Machinery, 2013. URL: https://doi.org/10.1145/2500365.2500597.
  2. Patrick Bahr, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. The clocks are ticking: No more delays! In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005097.
  3. Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters. Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science, 30(2):118-138, 2020. URL: https://doi.org/10.1017/S0960129519000197.
  4. Lars Birkedal, Rasmus Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:1)2012.
  5. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal. Guarded Dependent Type Theory with Coinductive Types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, pages 20-35. Springer Berlin Heidelberg, 2016. Google Scholar
  6. Sylvain Boulmé and Grégoire Hamon. Certifying synchrony for free. In Robert Nieuwenhuis and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, pages 495-506, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  7. Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. Programming and reasoning with guarded recursion for coinductive types. In Andrew Pitts, editor, Foundations of Software Science and Computation Structures, pages 407-421. Springer Berlin Heidelberg, 2015. Google Scholar
  8. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 120-134, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-61780-9_66.
  9. Daniel Gratzer. Normalization for multimodal type theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. URL: https://doi.org/10.1145/3531130.3532398.
  10. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal Dependent Type Theory. Logical Methods in Computer Science, Volume 17, Issue 3, July 2021. URL: https://doi.org/10.46298/lmcs-17(3:11)2021.
  11. Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi, 2022. URL: http://arxiv.org/abs/2202.12012.
  12. Adrien Guatto. A generalized modality for recursion. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209148.
  13. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous data flow programming language lustre. Proceedings of the IEEE, 79(9):1305-1320, 1991. URL: https://doi.org/10.1109/5.97300.
  14. Nicolas Halbwachs. Synchronous programming of reactive systems. In Alan J. Hu and Moshe Y. Vardi, editors, Computer Aided Verification, pages 1-16, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  15. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, pages 153-164, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  16. Martin Hofmann and Thomas Streicher. Lifting Grothendieck universes. Unpublished note, 1997. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  17. Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. Greatest hits: Higher inductive types in coinductive definitions via induction under clocks, 2021. URL: http://arxiv.org/abs/2102.01969.
  18. Bassel Mannaa, Rasmus Ejlers Møgelberg, and Niccolò Veltri. Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory. Logical Methods in Computer Science, Volume 16, Issue 4, December 2020. URL: https://doi.org/10.23638/LMCS-16(4:17)2020.
  19. Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, 2014. URL: https://doi.org/10.1145/2603088.2603132.
  20. H. Nakano. A modality for recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), pages 255-266. IEEE Computer Society, 2000. Google Scholar
  21. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  22. François Pottier. A typed store-passing translation for general references. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, January 2011. URL: https://doi.org/10.1145/1925844.1926403.
  23. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, 16(1), 2020. URL: http://arxiv.org/abs/1706.07526.
  24. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5):1203-1277, 2015. URL: https://doi.org/10.1017/S0960129514000565.
  25. Philipp Stassen, Daniel Gratzer, and Lars Birkedal. A flexible multimodal proof assistant, 2022. To appear in Workshop on the Implementation of Type Systems 2022. Google Scholar
  26. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, 2021. CMU technical report CMU-CS-21-142. URL: https://doi.org/10.5281/zenodo.5709838.
  27. Niccolò Veltri and Andrea Vezzosi. Formalizing π-calculus in guarded cubical agda. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 270-283, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact