{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:34:09Z","timestamp":1770248049619,"version":"3.49.0"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    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 meta language and obtain interoperability between the embedded language and the metalanguage. The existing Sikkel library for Agda achieves this for Multimode\n                    <jats:italic toggle=\"yes\">Simple<\/jats:italic>\n                    Type Theory (MSTT) with an internal presheaf model of\n                    <jats:italic toggle=\"yes\">dependent<\/jats:italic>\n                    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 \u00b5LF 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 \u00b5LF by proving some properties about functions manipulating guarded streams and by implementing an example involving parametricity predicates.\n                  <\/jats:p>","DOI":"10.1145\/3704844","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"210-240","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["BiSikkel: A Multimode Logical Framework in Agda"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9582-0789","authenticated-orcid":false,"given":"Joris","family":"Ceulemans","sequence":"first","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1571-5063","authenticated-orcid":false,"given":"Andreas","family":"Nuyts","sequence":"additional","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"KU Leuven, Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_2_3_1","volume-title":"A Polymorphic Lambda-Calculus with Sized Higher-Order Types","author":"Abel Andreas","year":"2006","unstructured":"Andreas Abel. 2006. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Ph. D. Dissertation. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006853"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_3_2_8_1","unstructured":"The Agda Community. 2024. A Standard Library for Cubical Agda. https:\/\/github.com\/agda\/cubical"},{"key":"e_1_3_2_9_1","unstructured":"The Agda Development Team. 2024. Agda. https:\/\/wiki.portal.chalmers.se\/agda"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_1"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.33"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"key":"e_1_3_2_17_1","unstructured":"Jeremy Avigad Leonardo de Moura and Soonho Kong. 2017. Theorem Proving in Lean. https:\/\/leanprover.github.io\/theorem_proving_in_lean\/index.html"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_3_2_19_1","first-page":"65","article-title":"Strict Syntax of Type Theory via Alpha-normalisation","author":"Bense Viktor","year":"2024","unstructured":"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\u201367. https:\/\/types2024.itu.dk\/abstracts.pdf#page=75","journal-title":"30th International Conference on Types for Proofs and Programs (TYPES)"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.360.5"},{"key":"e_1_3_2_24_1","unstructured":"Joris Ceulemans Andreas Nuyts and Dominique Devriese. 2024a. BiSikkel. https:\/\/github.com\/JorisCeulemans\/bisikkel"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Joris Ceulemans Andreas Nuyts and Dominique Devriese. 2024b. BiSikkel (a multimode logical framework in Agda) VM. https:\/\/doi.org\/10.5281\/zenodo.13939916 10.5281\/zenodo.13939916","DOI":"10.5281\/zenodo.13939916"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2023.4"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"James Chapman. 2009. Type Theory Should Eat Itself. Electronic Notes in Theoretical Computer Science 228 (2009) 21\u201336. https:\/\/doi.org\/10.1016\/j.entcs.2008.12.114 10.1016\/j.entcs.2008.12.114 Proceedings of the International Workshop on Logical Frameworks and Metalangu ages: Theory and Practice (LFMTP 2008).","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(3:7)2016"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628139"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498715"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.23"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_3_2_36_1","unstructured":"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"},{"key":"e_1_3_2_37_1","first-page":"79","volume-title":"Syntax and Semantics of Dependent Types","author":"Hofmann Martin","year":"1997","unstructured":"Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. Cambridge University Press, Cambridge, Chapter 4, 79\u2013130."},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935320"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.49"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.026"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.22"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27683-0_16"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_2"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_47_1","unstructured":"nLab authors. 2024. Functoriality of Categories of Presheaves. https:\/\/ncatlab.org\/nlab\/show\/functoriality+of+categories+of+presheaves Revision 7."},{"key":"e_1_3_2_48_1","unstructured":"Paige Randall North. 2018. Towards a Directed Homotopy Type Theory. CoRR abs\/1807.10566 (2018) 17 pages. arXiv:1807.10566 http:\/\/arxiv.org\/abs\/1807.10566"},{"key":"e_1_3_2_49_1","unstructured":"Andreas Nuyts. 2023a. 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"},{"key":"e_1_3_2_50_1","unstructured":"Andreas Nuyts. 2023b. 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"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209119"},{"key":"e_1_3_2_52_1","first-page":"4","article-title":"Menkar: Towards a Multimode Presheaf Proof Assistant","author":"Nuyts Andreas","year":"2019","unstructured":"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","journal-title":"TYPES"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(2:16)2024"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932499"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_2_57_1","unstructured":"Josselin Poiret Lucas Escot Joris Ceulemans Malin Altenm\u00fcller 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"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_16"},{"key":"e_1_3_2_59_1","first-page":"513","volume-title":"Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983","author":"Reynolds John C","year":"1983","unstructured":"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\u2013523."},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.12300"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2022.6"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.31"},{"key":"e_1_3_2_63_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373814"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:45Z","timestamp":1770200085000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":64,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704844"],"URL":"https:\/\/doi.org\/10.1145\/3704844","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}