BiSikkel: A Multimode Logical Framework in Agda
Article No.: 8, Pages 210 - 240
Abstract
Embedding Multimode Type Theory (MTT) as a library enables the usage of additional reasoning principles in off-the-shelf proof assistants without risking soundness or compatibility. Moreover, by interpreting embedded MTT terms in an internally constructed model of MTT, we can extract programs and proofs to the metalanguage and obtain interoperability between the embedded language and the metalanguage. The existing Sikkel library for Agda achieves this for Multimode Simple Type Theory (MSTT) with an internal presheaf model of dependent MTT. In this work, we add, on top of the simply-typed layer, a logical framework in which users can write multimode proofs about multimode Sikkel programs, still in an off-the-shelf proof assistant. To this end, we carve out of MTT a new multimode logical framework µLF over MSTT and implement it on top of Sikkel, interpreting both in the existing internal model. In the process, we further extend and improve the original codebase for each of the three layers (syntax, semantics and extraction) of Sikkel. We demonstrate the use of µLF by proving some properties about functions manipulating guarded streams and by implementing an example involving parametricity predicates.
References
[1]
Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Containers: Constructing Strictly Positive Types. Theoretical Computer Science, 342, 1 (2005), 3–27. issn:0304-3975 https://doi.org/10.1016/j.tcs.2005.06.002
[2]
Andreas Abel. 2006. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Ph. D. Dissertation. Ludwig-Maximilians-Universität München.
[3]
Andreas Abel. 2008. Polarised Subtyping for Sized Types. Mathematical Structures in Computer Science, 18, 5 (2008), 797–822. https://doi.org/10.1017/S0960129508006853
[4]
Andreas Abel, Joakim Öhman, and Andrea Vezzosi. 2017. Decidability of Conversion for Type Theory in Type Theory. Proc. ACM Program. Lang., 2, POPL (2017), Article 23, dec, 29 pages. https://doi.org/10.1145/3158111
[5]
Andreas Abel and Gabriel Scherer. 2012. On Irrelevance and Algorithmic Equality in Predicative Type Theory. Logical Methods in Computer Science, Volume 8, Issue 1 (2012), March, 1–36. https://doi.org/10.2168/LMCS-8(1:29)2012
[6]
Andreas Abel, Andrea Vezzosi, and Theo Winterhalter. 2017. Normalization by Evaluation for Sized Dependent Types. Proc. ACM Program. Lang., 1, ICFP (2017), Article 33, Aug., 30 pages. issn:2475-1421 https://doi.org/10.1145/3110277
[7]
The Agda Community. 2024. A Standard Library for Cubical Agda. https://github.com/agda/cubical
[8]
The Agda Development Team. 2024. Agda. https://wiki.portal.chalmers.se/agda
[9]
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2021. A Type- and Scope-safe Universe of Syntaxes with Binding: Their Semantics and Proofs. J. Funct. Program., 31 (2021), e22. https://doi.org/10.1017/S0956796820000076
[10]
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. 2021. Constructing a Universe for the Setoid Model. In Foundations of Software Science and Computation Structures, Stefan Kiefer and Christine Tasson (Eds.). Springer International Publishing, Cham. 1–21. isbn:978-3-030-71995-1 https://doi.org/10.1007/978-3-030-71995-1_1
[11]
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. 2018. Quotient Inductive-Inductive Types. In Foundations of Software Science and Computation Structures, Christel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham. 293–310. isbn:978-3-319-89366-2 https://doi.org/10.1007/978-3-319-89366-2_16
[12]
Thorsten Altenkirch and Ambrus Kaposi. 2016. Type Theory in Type Theory Using Quotient Inductive Types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). Association for Computing Machinery, New York, NY, USA. 18–29. isbn:9781450335492 https://doi.org/10.1145/2837614.2837638
[13]
Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. 2007. Observational Equality, Now!. In Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (PLPV ’07). Association for Computing Machinery, New York, NY, USA. 57–68. isbn:9781595936776 https://doi.org/10.1145/1292597.1292608
[14]
Thorsten Altenkirch and Peter Morris. 2009. Indexed Containers. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA. IEEE Computer Society, Washington D.C. 277–285. https://doi.org/10.1109/LICS.2009.33
[15]
Robert Atkey and Conor McBride. 2013. Productive Coprogramming with Guarded Recursion. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP ’13). Association for Computing Machinery, New York, NY, USA. 197–208. isbn:9781450323260 https://doi.org/10.1145/2500365.2500597
[16]
Jeremy Avigad, Leonardo de Moura, and Soonho Kong. 2017. Theorem Proving in Lean. https://leanprover.github.io/theorem_proving_in_lean/index.html
[17]
Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions as a Programming Language with Dependent Types. Springer Berlin Heidelberg, Berlin, Heidelberg. 365–379. https://doi.org/10.1007/978-3-540-78499-9_26
[18]
Viktor Bense, Ambrus Kaposi, and Szumi Xie. 2024. Strict Syntax of Type Theory via Alpha-normalisation. In 30th International Conference on Types for Proofs and Programs (TYPES). 65–67. https://types2024.itu.dk/abstracts.pdf##page=75
[19]
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters. 2020. Modal Dependent Type Theory and Dependent Right Adjoints. Mathematical Structures in Computer Science, 30, 2 (2020), 118–138. https://doi.org/10.1017/S0960129519000197
[20]
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. First Steps in Synthetic Guarded Domain Theory: Step-indexing in the Topos of Trees. Logical Methods in Computer Science, Volume 8, Issue 4 (2012), Oct., 45 pages. https://doi.org/10.2168/LMCS-8(4:1)2012
[21]
John Cartmell. 1986. Generalised Algebraic Theories and Contextual Categories. Ann. Pure Appl. Log., 32 (1986), 209–243. https://doi.org/10.1016/0168-0072(86)90053-9
[22]
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. 2022. Sikkel: Multimode Simple Type Theory as an Agda Library. In Proceedings Ninth Workshop on Mathematically Structured Functional Programming, Jeremy Gibbons and Max S. New (Eds.) (Electronic Proceedings in Theoretical Computer Science, Vol. 360). Open Publishing Association, Munich, Germany, 2nd April 2022. 93–112. https://doi.org/10.4204/EPTCS.360.5
[23]
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. 2024. BiSikkel. https://github.com/JorisCeulemans/bisikkel
[24]
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. 2024. BiSikkel (a multimode logical framework in Agda) VM. https://doi.org/10.5281/zenodo.13939916
[25]
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. 2024. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023), Delia Kesner, Eduardo Hermo Reyes, and Benno van den Berg (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 303). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 4:1–4:23. isbn:978-3-95977-332-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.TYPES.2023.4
[26]
James Chapman. 2009. Type Theory Should Eat Itself. Electronic Notes in Theoretical Computer Science, 228 (2009), 21–36. issn:1571-0661 https://doi.org/10.1016/j.entcs.2008.12.114 Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008)
[27]
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2017. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science, Volume 12, Issue 3 (2017), April, 39 pages. https://doi.org/10.2168/LMCS-12(3:7)2016
[28]
Jesper Cockx, Dominique Devriese, and Frank Piessens. 2014. Pattern Matching without K. SIGPLAN Not., 49, 9 (2014), aug, 257–268. issn:0362-1340 https://doi.org/10.1145/2692915.2628139
[29]
Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), Tarmo Uustalu (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 69). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 5:1–5:34. isbn:978-3-95977-030-9 issn:1868-8969 https://doi.org/10.4230/LIPIcs.TYPES.2015.5
[30]
Marcelo Fiore and Dmitrij Szamozvancev. 2022. Formal Metatheory of Second-order Abstract Syntax. Proc. ACM Program. Lang., 6, POPL (2022), 1–29. https://doi.org/10.1145/3498715
[31]
Daniel Gratzer. 2022. Normalization for Multimodal Type Theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’22). Association for Computing Machinery, New York, NY, USA. Article 2, 13 pages. isbn:9781450393515 https://doi.org/10.1145/3531130.3532398
[32]
Daniel Gratzer and Lars Birkedal. 2022. A Stratified Approach to Löb Induction. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), Amy P. Felty (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 228). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 23:1–23:22. isbn:978-3-95977-233-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2022.23
[33]
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2021. Multimodal Dependent Type Theory. Logical Methods in Computer Science, Volume 17, Issue 3 (2021), July, 67 pages. https://doi.org/10.46298/lmcs-17(3:11)2021
[34]
Adrien Guatto. 2018. A Generalized Modality for Recursion. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Association for Computing Machinery, New York, NY, USA. 482–491. isbn:9781450355834 https://doi.org/10.1145/3209108.3209148
[35]
Martin Hofmann. 1995. Extensional Concepts in Intensional Type Theory. Ph. D. Dissertation. University of Edinburgh. College of Science and Engineering. https://era.ed.ac.uk/handle/1842/399
[36]
Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. Cambridge University Press, Cambridge. 79–130.
[37]
Jason Z. S. Hu and Jacques Carette. 2021. Formalizing Category Theory in Agda. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021). Association for Computing Machinery, New York, NY, USA. 327–342. isbn:9781450382991 https://doi.org/10.1145/3437992.3439922
[38]
Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. 2016. The Definitional Side of the Forcing. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’16). Association for Computing Machinery, New York, NY, USA. 367–376. isbn:9781450343916 https://doi.org/10.1145/2933575.2935320
[39]
Guilhem Jaber, Nicolas Tabareau, and Matthieu Sozeau. 2012. Extending Type Theory with Forcing. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (LICS 2012). IEEE Computer Society Press, Washington D.C. 395–404. https://doi.org/10.1109/LICS.2012.49
[40]
Daniel R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. Electr. Notes Theor. Comput. Sci., 276 (2011), 263–289. https://doi.org/10.1016/j.entcs.2011.09.026
[41]
Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. 2018. Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Hélène Kirchner (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 22:1–22:17. isbn:978-3-95977-077-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2018.22
[42]
Daniel R. Licata and Michael Shulman. 2016. Adjoint Logic with a 2-Category of Modes. In Logical Foundations of Computer Science - International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings, Sergei N. Artëmov and Anil Nerode (Eds.) (Lecture Notes in Computer Science, Vol. 9537). Springer, Cham. 219–235. https://doi.org/10.1007/978-3-319-27683-0_16
[43]
Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer, Berlin, Heidelberg. 344–359. https://doi.org/10.1007/3-540-45413-6_27
[44]
Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures, Roberto Amadio (Ed.). Springer, Berlin, Heidelberg. 350–364. https://doi.org/10.1007/978-3-540-78499-9_25
[45]
Hiroshi Nakano. 2000. A Modality for Recursion. In Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science. IEEE, Washington D.C. 255–266. issn:1043-6871 https://doi.org/10.1109/LICS.2000.855774
[46]
nLab authors. 2024. Functoriality of Categories of Presheaves. https://ncatlab.org/nlab/show/functoriality+of+categories+of+presheaves
[47]
Paige Randall North. 2018. Towards a Directed Homotopy Type Theory. CoRR, abs/1807.10566 (2018), 17 pages. arXiv:1807.10566. arxiv:1807.10566
[48]
Andreas Nuyts. 2023. Higher Pro-arrows: Towards a Model for Naturality Pretype Theory. In Workshop on Homotopy Type Theory / Univalent Foundations. 4 pages. https://hott-uf.github.io/2023/HoTTUF_2023_paper_1410.pdf
[49]
Andreas Nuyts. 2023. A Lock Calculus for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES). 3 pages. https://lirias.kuleuven.be/retrieve/720873
[50]
Andreas Nuyts and Dominique Devriese. 2018. Degrees of Relatedness: A Unified Framework for Parametricity, Irrelevance, Ad Hoc Polymorphism, Intersections, Unions and Algebra in Dependent Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). Association for Computing Machinery, New York, NY, USA. 779–788. isbn:9781450355834 https://doi.org/10.1145/3209108.3209119
[51]
Andreas Nuyts and Dominique Devriese. 2019. Menkar: Towards a Multimode Presheaf Proof Assistant. In TYPES. 4 pages. https://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_33
[52]
Andreas Nuyts and Dominique Devriese. 2024. Transpension: The Right Adjoint to the Pi-type. Logical Methods in Computer Science, Volume 20, Issue 2 (2024), June, 54 pages. https://doi.org/10.46298/lmcs-20(2:16)2024
[53]
Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017. Parametric Quantifiers for Dependent Type Theory. Proc. ACM Program. Lang., 1, ICFP (2017), Article 32, Aug., 29 pages. https://doi.org/10.1145/3110276
[54]
Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In LICS ’01. IEEE, Washington D.C. 221–230. https://doi.org/10.1109/LICS.2001.932499
[55]
Frank Pfenning and Rowan Davies. 2001. A Judgmental Reconstruction of Modal Logic. Mathematical Structures in Computer Science, 11, 4 (2001), 511–540. https://doi.org/10.1017/S0960129501003322
[56]
Josselin Poiret, Lucas Escot, Joris Ceulemans, Malin Altenmüller, and Andreas Nuyts. 2023. Read the Mode and Stay Positive. In 29th International Conference on Types for Proofs and Programs (TYPES). 3 pages. https://lirias.kuleuven.be/retrieve/720869
[57]
Jason Reed. 2003. Extending Higher-Order Unification to Support Proof Irrelevance. In Theorem Proving in Higher Order Logics, David Basin and Burkhart Wolff (Eds.). Springer, Berlin, Heidelberg. 238–252. https://doi.org/10.1007/10930755_16
[58]
John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983, R. E. A. Mason (Ed.). North-Holland/IFIP, Amsterdam. 513–523.
[59]
Michael Shulman. 2023. Semantics of Multimodal Adjoint Type Theory. Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX (2023), Nov., 19 pages. https://doi.org/10.46298/entics.12300
[60]
Philipp Stassen, Daniel Gratzer, and Lars Birkedal. 2023. mitten: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), Delia Kesner and Pierre-Marie Pédrot (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 269). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 6:1–6:23. isbn:978-3-95977-285-3 issn:1868-8969 https://doi.org/10.4230/LIPIcs.TYPES.2022.6
[61]
Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. 2019. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 31:1–31:25. isbn:978-3-95977-107-8 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2019.31
[62]
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book Institute for Advanced Study.
[63]
Niccolò Veltri and Andrea Vezzosi. 2020. Formalizing π -Calculus in Guarded Cubical Agda. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020). Association for Computing Machinery, New York, NY, USA. 270–283. isbn:9781450370974 https://doi.org/10.1145/3372885.3373814
[64]
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2021. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. J. Funct. Program., 31 (2021), e8. https://doi.org/10.1017/S0956796821000034
Index Terms
- BiSikkel: A Multimode Logical Framework in Agda
Recommendations
Parametric quantifiers for dependent type theory
Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...
Embedding a logical theory of constructions in Agda
PLPV '09: Proceedings of the 3rd workshop on Programming languages meets program verificationWe propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-Löf's intuitionistic type theory. We show how to embed an external programming logic, Aczel's Logical ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2025
2363 pages
Copyright © 2025 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2025
Published in PACMPL Volume 9, Issue POPL
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- Research Foundation ? Flanders (FWO)
- Research Fund and Internal Funds KU Leuven
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 104Total Downloads
- Downloads (Last 12 months)104
- Downloads (Last 6 weeks)104
Reflects downloads up to 18 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in