Document Open Access Logo

A Sound and Complete Substitution Algorithm for Multimode Type Theory

Authors Joris Ceulemans , Andreas Nuyts , Dominique Devriese

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2023.4.pdf
  • Filesize: 0.93 MB
  • 23 pages

Document Identifiers

Author Details

Joris Ceulemans
  • DistriNet, KU Leuven, Belgium
Andreas Nuyts
  • DistriNet, KU Leuven, Belgium
Dominique Devriese
  • DistriNet, KU Leuven, Belgium

Funding

  • Ceulemans, Joris: Held a PhD fellowship (1184122N) of the Research Foundation - Flanders (FWO) while working on this research. This research is partially funded by the Research Fund KU Leuven and by the Research Foundation - Flanders (FWO; G030320N).
  • Nuyts, Andreas: Holds a Postdoctoral fellowship (1247922N) of the Research Foundation - Flanders (FWO).

Cite AsGet BibTex

Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.TYPES.2023.4

Abstract

Multimode Type Theory (MTT) is a generic type theory that can be instantiated with an arbitrary mode theory to model features like parametricity, cohesion and guarded recursion. However, the presence of modalities in MTT significantly complicates the substitution calculus of this system. Moreover, MTT’s syntax has explicit substitutions with an axiomatic system - not an algorithm - governing the connection between an explicitly substituted term and the resulting term in which variables have actually been replaced. So far, the only results on eliminating explicit substitutions in MTT rely on normalisation by evaluation and hence also immediately normalise a term. In this paper, we present a substitution algorithm for MTT that is completely separated from normalisation. To this end, we introduce Substitution-Free Multimode Type Theory (SFMTT): a formulation of MTT without explicit substitutions, but for which we are able to give a structurally recursive substitution algorithm, suitable for implementation in a total programming language or proof assistant. On the usual formulation of MTT, we consider σ-equality, the congruence generated solely by equality rules for explicit substitutions. There is a trivial embedding from SFMTT to MTT, and a converse translation that eliminates the explicit substitutions. We prove soundness and completeness of our algorithm with respect to σ-equivalence and thus establish that MTT with σ-equality has computable σ-normal forms, given by the terms of SFMTT.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Modal and temporal logics
  • Software and its engineering → Syntax
Keywords
  • dependent type theory
  • modalities
  • multimode type theory
  • explicit substitutions
  • substitution algorithm

Metrics

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

Supplementary Materials

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit substitutions. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 31-46, New York, NY, USA, 1989. Association for Computing Machinery. URL: https://doi.org/10.1145/96709.96712.
  2. Andreas Abel. Polarised subtyping for sized types. Mathematical Structures in Computer Science, 18(5):797-822, 2008. URL: https://doi.org/10.1017/S0960129508006853.
  3. Andreas Abel. Normalization by evaluation: Dependent types and impredicativity. Habilitation thesis, Ludwig-Maximilians-Universität München, Germany, 2013. Google Scholar
  4. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. Journal of Functional Programming, 31:e22, 2021. URL: https://doi.org/10.1017/S0956796820000076.
  5. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182-199. Springer, 1995. URL: https://doi.org/10.1007/3-540-60164-3_27.
  6. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  7. Patrick Bahr, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. The clocks are ticking: No more delays! In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005097.
  8. Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. Electron. Notes in Theor. Comput. Sci., 319:67-82, 2015. URL: https://doi.org/10.1016/j.entcs.2015.12.006.
  9. Marc Bezem, Thierry Coquand, and Simon Huber. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26, pages 107-128, Dagstuhl, Germany, 2014. URL: https://doi.org/10.4230/LIPIcs.TYPES.2013.107.
  10. 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.
  11. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  12. Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. Sikkel: Multimode simple type theory as an agda library. In Jeremy Gibbons and Max S. New, editors, Proceedings Ninth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022, volume 360 of EPTCS, pages 93-112, 2022. URL: https://doi.org/10.4204/EPTCS.360.5.
  13. Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A sound and complete substitution algorithm for multimode type theory: Technical report. 2024. URL: https://doi.org/10.48550/arXiv.2406.13622.
  14. Ranald Clouston. Fitch-style modal lambda calculi. In Christel Baier and Ugo Dal Lago, editors, FOSSACS 2018, Held as Part of ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 258-275. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_14.
  15. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, volume 69 of LIPIcs, pages 5:1-5:34. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  16. Marcelo Fiore and Dmitrij Szamozvancev. Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang., 6(POPL):1-29, 2022. URL: https://doi.org/10.1145/3498715.
  17. Daniel Gratzer. Normalization for multimodal type theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, 2022. URL: https://doi.org/10.1145/3531130.3532398.
  18. Daniel Gratzer. PhD thesis, Aarhus University, Denmark, 2023. URL: Syntax and semantics of modal type theory.
  19. Daniel Gratzer, Alex Kavvos, Andreas Nuyts, and Lars Birkedal. Type theory à la mode. Pre-print, 2020. URL: https://lirias.kuleuven.be/retrieve/635295.
  20. 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.
  21. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a modal dependent type theory. Proc. ACM Program. Lang., pages 107:1-107:29, 2019. URL: https://doi.org/10.1145/3341711.
  22. Per Martin-Löf. Intuitionistic type theory. In Studies in proof theory. Bibliopolis, 1984. Google Scholar
  23. Conor McBride. Type-preserving renaming and substitution. Unpublished note, 2005. URL: http://strictlypositive.org/ren-sub.pdf.
  24. Andreas Nuyts. Contextual algebraic theories: Generic boilerplate beyond abstraction (extended abstract). In Workshop on Type-Driven Development (TyDe), September 2022. URL: https://anuyts.github.io/files/cmat-tyde22-abstract.pdf.
  25. Andreas Nuyts. A lock calculus for multimode type theory. In 29th International Conference on Types for Proofs and Programs (TYPES), June 2023. URL: https://lirias.kuleuven.be/retrieve/720873.
  26. Andreas Nuyts and Dominique Devriese. Degrees of relatedness: A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory. In Logic in Computer Science (LICS) 2018, Oxford, UK, July 09-12, 2018, pages 779-788, 2018. URL: https://doi.org/10.1145/3209108.3209119.
  27. Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. Parametric quantifiers for dependent type theory. PACMPL, 1(ICFP):32:1-32:29, 2017. URL: https://doi.org/10.1145/3110276.
  28. Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In LICS '01, pages 221-230, 2001. URL: https://doi.org/10.1109/LICS.2001.932499.
  29. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511-540, 2001. URL: https://doi.org/10.1017/S0960129501003322.
  30. Philipp Stassen, Daniel Gratzer, and Lars Birkedal. mitten: A Flexible Multimodal Proof Assistant. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:23, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2022.6.
  31. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, USA, 2022. URL: https://doi.org/10.1184/R1/19632681.V1.
  32. Nachiappan Valliappan, Fabian Ruch, and Carlos Tomé Cortiñas. Normalization for fitch-style modal calculi. Proc. ACM Program. Lang., 6(ICFP), August 2022. URL: https://doi.org/10.1145/3547649.
  33. Niccolò Veltri and Andrea Vezzosi. Formalizing π-calculus in guarded cubical agda. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 270-283. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373814.
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