{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806816,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["742178"],"award-info":[{"award-number":["742178"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575679","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"78-89","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Encoding Dependently-Typed Constructions into Simple Type Theory"],"prefix":"10.1145","author":[{"given":"Anthony","family":"Bordg","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Adri\u00e1n","family":"Do\u00f1a Mateo","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL","author":"Altenkirch Thorsten","year":"2016","unstructured":"Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2631172.2631176"},{"key":"e_1_3_2_1_3_1","unstructured":"Dimitri Ara. 2010. Sur les \u221e -groupo\u00efdes de Grothendieck et une variante \u221e -cat\u00e9gorique. Ph. D. Dissertation. Universit\u00e9 Paris 7. https:\/\/www.i2m.univ-amu.fr\/perso\/dimitri.ara\/files\/these.pdf"},{"key":"e_1_3_2_1_4_1","volume-title":"Serbia (May","author":"Assaf Ali","year":"2016","unstructured":"Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Fr\u00e9d\u00e9ric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. 2016. Expressing theories in the \u03bb \u03a0 -calculus modulo theory and in the Dedukti system. TYPES: Types for Proofs and Programs. Novi SAd, Serbia (May 2016)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09537-9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1998.1724"},{"key":"e_1_3_2_1_8_1","volume-title":"Some Axioms for Mathematics. In FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction.","author":"Blanqui Fr\u00e9d\u00e9ric","year":"2021","unstructured":"Fr\u00e9d\u00e9ric Blanqui, Gilles Dowek, \u00c9milie Grienenberger, Gabriel Hondet, and Fran\u00e7ois Thir\u00e9. 2021. Some Axioms for Mathematics. In FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.195.6"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_3_2_1_11_1","unstructured":"Anthony Bordg. 2018. Projective Geometry. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Projective_Geometry.html"},{"key":"e_1_3_2_1_12_1","unstructured":"Anthony Bordg. 2022. How to Do Maths Without Dependent Types. available at. https:\/\/sites.google.com\/site\/anthonybordg\/home"},{"key":"e_1_3_2_1_13_1","unstructured":"Anthony Bordg and Nicol\u00f2 Cavalleri. 2021. Elements of Differential Geometry in Lean: A Report for Mathematicians. To appear in the proceedings of FMM 2021 - Fifth Workshop on Formal Mathematics for Mathematicians arXiv preprint arXiv:2108.00484"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09584-7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Anthony Bordg Lawrence Paulson and Wenda Li. 2022. Simple Type Theory is not too Simple: Grothendieck\u2019s Schemes Without Dependent Types. Experimental Mathematics 1\u201319.","DOI":"10.1080\/10586458.2022.2062073"},{"key":"e_1_3_2_1_16_1","unstructured":"Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph. D. Dissertation. Universit\u00e9 de Nice Sophia Antipolis. arXiv preprint arXiv:1606.05916"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373830"},{"key":"e_1_3_2_1_18_1","volume-title":"Ramon Fern\u00e1ndez Mir, and Scott Morrison","author":"Buzzard Kevin","year":"2021","unstructured":"Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fern\u00e1ndez Mir, and Scott Morrison. 2021. Schemes in Lean. Experimental Mathematics, 1\u20139."},{"key":"e_1_3_2_1_19_1","unstructured":"Laurent Igal Chicli. 2003. Sur la formalisation des math\u00e9matiques dans le Calcul des Constructions Inductives. Ph. D. Dissertation. Universit\u00e9 de Nice."},{"key":"e_1_3_2_1_20_1","unstructured":"Floris Cnossen. 2021. Simplicial sets in Lean. Bachelor thesis"},{"key":"e_1_3_2_1_21_1","first-page":"1085","article-title":"Th\u00e9orie des types d\u00e9pendants et axiome d\u2019univalence","volume":"66","author":"Coquand Thierry","year":"2014","unstructured":"Thierry Coquand. 2014. Th\u00e9orie des types d\u00e9pendants et axiome d\u2019univalence. S\u00e9minaire Bourbaki, 66 (2014), 1085.","journal-title":"S\u00e9minaire Bourbaki"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(75)90015-8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_30"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005124"},{"key":"e_1_3_2_1_25_1","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier. 2008. Formal proof\u2013the four-color theorem. Notices of the AMS, 55, 11 (2008), 1382\u20131393.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_28_1","volume-title":"John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, and Tat Thang Nguyen.","author":"Hales Thomas","year":"2017","unstructured":"Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, and Tat Thang Nguyen. 2017. A formal proof of the Kepler conjecture. In Forum of mathematics, Pi. 5."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000528"},{"key":"e_1_3_2_1_30_1","volume-title":"13th International Conference on Typed Lambda Calculi and Applications (TLCA","author":"Hirschowitz Andr\u00e9","year":"2015","unstructured":"Andr\u00e9 Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. 2015. Wild omega-categories for the homotopy hypothesis in type theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_3_2_1_32_1","unstructured":"Gabriel Hondet and Fr\u00e9d\u00e9ric Blanqui. 2020. The New Rewriting Engine of Dedukti. arXiv preprint arXiv:2010.16115."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294093"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"key":"e_1_3_2_1_36_1","volume-title":"Coq. TYPES","author":"Lafont Ambroise","year":"2018","unstructured":"Ambroise Lafont, Tom Hirschowitz, and Nicolas Tabareau. 2018. Types are weak omega-groupoids, in Coq. TYPES 2018."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319317"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Tom Leinster. 2004. Higher Operads Higher Categories. Cambridge University Press. isbn:9780521532150 lccn:2003055356","DOI":"10.1017\/CBO9780511525896"},{"key":"e_1_3_2_1_39_1","volume-title":"Weak \u03c9 -Categories from Intensional Type Theory. Logical Methods in Computer Science, 6","author":"LeFanu Lumsdaine Peter","year":"2010","unstructured":"Peter LeFanu Lumsdaine. 2010. Weak \u03c9 -Categories from Intensional Type Theory. Logical Methods in Computer Science, 6 (2010)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comgeo.2010.06.004"},{"volume-title":"Studies in Logic and the Foundations of Mathematics. 80","author":"Martin-L\u00f6f Per","key":"e_1_3_2_1_41_1","unstructured":"Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Studies in Logic and the Foundations of Mathematics. 80, Elsevier, 73\u2013118."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"e_1_3_2_1_44_1","unstructured":"Arnaud Spiwack. 2011. Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory. Ph. D. Dissertation."},{"key":"e_1_3_2_1_45_1","unstructured":"Eugene W. Stark. 2016. Category Theory with Adjunctions and Limits. Archive of Formal Proofs June issn:2150-914x https:\/\/isa-afp.org\/entries\/Category3.html"},{"volume-title":"Towards higher categories","author":"Street Ross","key":"e_1_3_2_1_46_1","unstructured":"Ross Street. 2010. An Australian conspectus of higher categories. In Towards higher categories. Springer, 237\u2013264."},{"key":"e_1_3_2_1_47_1","unstructured":"Thomas Streicher. 1993. Investigations into intensional type theory. Habilitiation Thesis Ludwig Maximilian Universit\u00e4t."},{"key":"e_1_3_2_1_48_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_3_2_1_50_1","volume-title":"Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14","author":"Vicary Jamie","year":"2018","unstructured":"Jamie Vicary, Aleks Kissinger, and Krzysztof Bar. 2018. Globular: an online proof assistant for higher-dimensional rewriting. Logical Methods in Computer Science, 14 (2018)."},{"key":"e_1_3_2_1_51_1","unstructured":"Vladimir Voevodsky. May 11 2014. A simple type system with two identity types. An unfinished unreleased (?) manuscript"},{"key":"e_1_3_2_1_52_1","unstructured":"Vladimir Voevodsky. September 2006. A very short note on homotopy \u03bb -calculus. http:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf Unpublished 7 pages"},{"key":"e_1_3_2_1_53_1","unstructured":"Vladimir Voevodsky. September 8 2009. Notes on type systems. Unpublished"},{"key":"e_1_3_2_1_54_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens and Daniel Grayson. 2014. UniMath \u2014 a computer-checked library of univalent mathematics. available at. https:\/\/unimath.org"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028402"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575679","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575679","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575679"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":54,"alternative-id":["10.1145\/3573105.3575679","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575679","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}