{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:20Z","timestamp":1776316940869,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209207","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"739-748","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Dialectica models of type theory"],"prefix":"10.1145","author":[{"given":"Sean K.","family":"Moss","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford"}]},{"given":"Tamara","family":"von Glehn","sequence":"additional","affiliation":[{"name":"Department of Pure Mathematics and Mathematical Statistics, University of Cambridge"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754809.1754813"},{"key":"e_1_3_2_1_2_1","volume-title":"Higher-order Containers. In Proceedings of the Programs, Proofs, Process and 6th International Conference on Computability in Europe (CiE '10)","author":"Altenkirch Thorsten","year":"2010","unstructured":"Thorsten Altenkirch , Paul Levy , and Sam Staton . 2010 . Higher-order Containers. In Proceedings of the Programs, Proofs, Process and 6th International Conference on Computability in Europe (CiE '10) . Springer-Verlag, 11--20. http:\/\/dl.acm.org\/citation.cfm?id= 1876420.1876422 Thorsten Altenkirch, Paul Levy, and Sam Staton. 2010. Higher-order Containers. In Proceedings of the Programs, Proofs, Process and 6th International Conference on Computability in Europe (CiE '10). Springer-Verlag, 11--20. http:\/\/dl.acm.org\/citation.cfm?id=1876420.1876422"},{"key":"e_1_3_2_1_3_1","volume-title":"Stud. Logic Found. Math.","volume":"137","author":"Avigad Jeremy","year":"1998","unstructured":"Jeremy Avigad and Solomon Feferman . 1998 . G\u00f6del's functional (\"Dialectica\") interpretation. In Handbook of proof theory . Stud. Logic Found. Math. , Vol. 137 . North-Holland, Amsterdam, 337--405. Jeremy Avigad and Solomon Feferman. 1998. G\u00f6del's functional (\"Dialectica\") interpretation. In Handbook of proof theory. Stud. Logic Found. Math., Vol. 137. North-Holland, Amsterdam, 337--405."},{"key":"e_1_3_2_1_4_1","volume-title":"19th International Conference on Types for Proofs and Programs (TYPES 2013) (Leibniz International Proceedings in Informatics (LIPIcs)), Ralph Matthes and Aleksy Schubert (Eds.)","volume":"26","author":"Bezem Marc","year":"2014","unstructured":"Marc Bezem , Thierry Coquand , and Simon Huber . 2014 . A Model of Type Theory in Cubical Sets . In 19th International Conference on Types for Proofs and Programs (TYPES 2013) (Leibniz International Proceedings in Informatics (LIPIcs)), Ralph Matthes and Aleksy Schubert (Eds.) , Vol. 26 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 107--128. Marc Bezem, Thierry Coquand, and Simon Huber. 2014. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013) (Leibniz International Proceedings in Informatics (LIPIcs)), Ralph Matthes and Aleksy Schubert (Eds.), Vol. 26. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 107--128."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.07.004"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90035-R"},{"key":"e_1_3_2_1_7_1","volume-title":"Quantum Physics and Linguistics","author":"Coumans Dion","unstructured":"Dion Coumans and Bart Jacobs . 2013. Scalars, Monads, and Categories. In Quantum Physics and Linguistics . Oxford University Press , 184--216. Dion Coumans and Bart Jacobs. 2013. Scalars, Monads, and Categories. In Quantum Physics and Linguistics. Oxford University Press, 184--216."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02025118"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(97)00129-1"},{"key":"e_1_3_2_1_15_1","unstructured":"J.M.E. Hyland J. van Oosten G. Rosolini T Streicher B. Biering L Birkedal and C Butz. 2007. Topos theoretic versions of Dialectica interpretations. (2007). unpublished draft.  J.M.E. Hyland J. van Oosten G. Rosolini T Streicher B. Biering L Birkedal and C Butz. 2007. Topos theoretic versions of Dialectica interpretations. (2007). unpublished draft."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00075-6"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_3_2_1_18_1","volume-title":"Stud. Logic Found. Math.","volume":"141","author":"Jacobs Bart","year":"1999","unstructured":"Bart Jacobs . 1999 . Categorical logic and type theory . Stud. Logic Found. Math. , Vol. 141 . North-Holland, Amsterdam. xviii+760 pages. Bart Jacobs. 1999. Categorical logic and type theory. Stud. Logic Found. Math., Vol. 141. North-Holland, Amsterdam. xviii+760 pages."},{"key":"e_1_3_2_1_19_1","volume-title":"Sketches of an elephant: a topos theory compendium. Vols. 1-2. Oxford Logic Guides","author":"Johnstone Peter T.","unstructured":"Peter T. Johnstone . 2002. Sketches of an elephant: a topos theory compendium. Vols. 1-2. Oxford Logic Guides , Vol. 43- 44 . The Clarendon Press, Oxford University Press , New York . xxii+468--71 pages. Peter T. Johnstone. 2002. Sketches of an elephant: a topos theory compendium. Vols. 1-2. Oxford Logic Guides, Vol. 43-44. The Clarendon Press, Oxford University Press, New York. xxii+468--71 pages."},{"key":"e_1_3_2_1_20_1","volume-title":"Peter LeFanu Lumsdaine, and Vladimir Voevodsky","author":"Kapulkin Chris","year":"2012","unstructured":"Chris Kapulkin , Peter LeFanu Lumsdaine, and Vladimir Voevodsky . 2012 . The Simplicial Model of Univalent Foundations . (2012). arXiv:1211.2851 Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. 2012. The Simplicial Model of Univalent Foundations. (2012). arXiv:1211.2851"},{"key":"e_1_3_2_1_21_1","volume-title":"Applied proof theory: proof interpretations and their use in mathematics","author":"Kohlenbach U.","unstructured":"U. Kohlenbach . 2008. Applied proof theory: proof interpretations and their use in mathematics . Springer-Verlag , Berlin . xx+532 pages. U. Kohlenbach. 2008. Applied proof theory: proof interpretations and their use in mathematics. Springer-Verlag, Berlin. xx+532 pages."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"e_1_3_2_1_23_1","volume-title":"Reynolds","author":"Ma QingMing","year":"1992","unstructured":"QingMing Ma and John C . Reynolds . 1992 . Types, abstraction, and parametric polymorphism. II. In Mathematical foundations of programming semantics (Pittsburgh, PA, 1991). Lecture Notes in Comput. Sci., Vol. 598 . Springer , Berlin, 1--40. QingMing Ma and John C. Reynolds. 1992. Types, abstraction, and parametric polymorphism. II. In Mathematical foundations of programming semantics (Pittsburgh, PA, 1991). Lecture Notes in Comput. Sci., Vol. 598. Springer, Berlin, 1--40."},{"key":"e_1_3_2_1_24_1","volume-title":"Categories for the working mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane . 1998. Categories for the working mathematician ( 2 nd ed.). Graduate Texts in Mathematics, Vol. 5 . Springer-Verlag , New York. xii+314 pages. Saunders Mac Lane. 1998. Categories for the working mathematician (2nd ed.). Graduate Texts in Mathematics, Vol. 5. Springer-Verlag, New York. xii+314 pages.","edition":"2"},{"key":"e_1_3_2_1_25_1","volume-title":"Studies in Proof Theory. Lecture Notes","volume":"1","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f . 1984 . Intuitionistic type theory . Studies in Proof Theory. Lecture Notes , Vol. 1 . Bibliopolis, Naples. iv+91 pages. Notes by Giovanni Sambin. Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in Proof Theory. Lecture Notes, Vol. 1. Bibliopolis, Naples. iv+91 pages. Notes by Giovanni Sambin."},{"key":"e_1_3_2_1_27_1","first-page":"05","article-title":"Univalence for inverse diagrams and homotopy canonicity","volume":"25","author":"Shulman Michael","year":"2014","unstructured":"Michael Shulman . 2014 . Univalence for inverse diagrams and homotopy canonicity . Mathematical Structures in Computer Science 25 , 05 (November 2014), 1203--1277. Michael Shulman. 2014. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science 25, 05 (November 2014), 1203--1277.","journal-title":"Mathematical Structures in Computer Science"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2017.v19.n2.a12"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-009-9214-3"},{"key":"e_1_3_2_1_30_1","unstructured":"Thomas Streicher. 2018. Fibred Categories \u00e0 la Jean B\u00e9nabou. (2018). arXiv:1801.02927  Thomas Streicher. 2018. Fibred Categories \u00e0 la Jean B\u00e9nabou. (2018). arXiv:1801.02927"},{"key":"e_1_3_2_1_31_1","volume-title":"Practical foundations of mathematics","author":"Taylor Paul","unstructured":"Paul Taylor . 1999. Practical foundations of mathematics . Cambridge Studies in Advanced Mathematics, Vol. 59 . Cambridge University Press , Cambridge. xii+572 pages. http:\/\/paultaylor.eu\/~pt\/prafm\/ Paul Taylor. 1999. Practical foundations of mathematics. Cambridge Studies in Advanced Mathematics, Vol. 59. Cambridge University Press, Cambridge. xii+572 pages. http:\/\/paultaylor.eu\/~pt\/prafm\/"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra (Ed.). 1973. Metamathematical investigation of intuitionistic arithmetic and analysis. Springer-Verlag Berlin-New York. xvii+485 pages.  A. S. Troelstra (Ed.). 1973. Metamathematical investigation of intuitionistic arithmetic and analysis. Springer-Verlag Berlin-New York. xvii+485 pages.","DOI":"10.1007\/BFb0066739"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005084"}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Oxford United Kingdom","acronym":"LICS '18","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209207","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209207","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:08:24Z","timestamp":1750208904000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209207"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":30,"alternative-id":["10.1145\/3209108.3209207","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209207","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}