Document Open Access Logo

{mitten}: A Flexible Multimodal Proof Assistant

Authors Philipp Stassen , Daniel Gratzer , Lars Birkedal

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.6.pdf
  • Filesize: 0.91 MB
  • 23 pages

Document Identifiers

Author Details

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

Funding

This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.

Cite AsGet BibTex

Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.6

Abstract

Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Modal and temporal logics
Keywords
  • Dependent type theory
  • guarded recursion
  • modal type theory
  • proof assistants

Metrics

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

References

  1. Andreas Abel. Polarised subtyping for sized types. Mathematical Structures in Computer Science, 18(5):797-822, 2008. URL: https://doi.org/10.1017/S0960129508006853.
  2. Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation, Ludwig-Maximilians-Universität München, 2013. Google Scholar
  3. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158111.
  4. 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.
  5. Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. Simply ratt: A fitch-style modal calculus for reactive programming without space leaks. Proc. ACM Program. Lang., 3:109:1-109:27, 2019. URL: https://doi.org/10.1145/3341713.
  6. Magnus Baunsgaard Kristensen, Rasmus Ejlers Mogelberg, and Andrea Vezzosi. Greatest hits: Higher inductive types in coinductive definitions via induction under clocks. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533359.
  7. 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.
  8. 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.
  9. Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. Sikkel: Multimode simple type theory as an agda library. In Electronic Proceedings in Theoretical Computer Science, volume 360, pages 93-112. Munich, Germany, Open Publishing Association, June 2022. URL: https://doi.org/10.4204/EPTCS.360.5.
  10. 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
  11. Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1):167-177, 1996. URL: https://doi.org/10.1016/0167-6423(95)00021-6.
  12. Valeria de Paiva and Eike Ritter. Fibrational modal type theory. In Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), 2015. URL: https://doi.org/10.1016/j.entcs.2016.06.010.
  13. 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. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3532398.
  14. Daniel Gratzer and Lars Birkedal. A Stratified Approach to Löb Induction. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:22, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.23.
  15. 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.
  16. Daniel Gratzer, G.A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394736.
  17. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a Modal Dependent Type Theory. Proc. ACM Program. Lang., 3, 2019. URL: https://doi.org/10.1145/3341711.
  18. Jason Z. S. Hu and Brigitte Pientka. An investigation of kripke-style modal type theories, 2022. URL: https://doi.org/10.48550/arXiv.2206.07823.
  19. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In H. Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  20. Daniel R. Licata and Michael Shulman. Adjoint Logic with a 2-Category of Modes. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 219-235. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-27683-0_16.
  21. Daniel R. Licata, Michael Shulman, and Mitchell Riley. A Fibrational Framework for Substructural and Modal Logics. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.25.
  22. Rasmus Ejlers Møgelberg and Niccolò Veltri. Bisimulation as path type for guarded recursive types. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290317.
  23. Andreas Nuyts. Menkar. https://github.com/anuyts/menkar, 2019.
  24. Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856-941, 2018. URL: https://doi.org/10.1017/S0960129517000147.
  25. The Agda Team. Agda, 2022. URL: https://agda.readthedocs.io/en/latest/language/guarded-cubical.html.
  26. 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
  27. Vezzosi, Andrea. agda-flat, 2018. URL: https://github.com/agda/agda/tree/flat.
  28. Colin Zwanziger. Natural model semantics for comonadic and adjoint type theory: Extended abstract. In Preproceedings of Applied Category Theory Conference 2019, 2019. 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 Imprint Privacy Contact