{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:53:36Z","timestamp":1781855616051,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,7,9]],"date-time":"2019-07-09T00:00:00Z","timestamp":1562630400000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0053"],"award-info":[{"award-number":["FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209130","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T08:14:43Z","timestamp":1530087283000},"page":"76-85","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Impredicative Encodings of (Higher) Inductive Types"],"prefix":"10.1145","author":[{"given":"Steve","family":"Awodey","sequence":"first","affiliation":[{"name":"Department of Philosophy, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonas","family":"Frey","sequence":"additional","affiliation":[{"name":"Department of Philosophy, Carnegie Mellon University, Pittsburgh, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sam","family":"Speight","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_3_1","volume-title":"Impredicative Encodings in HoTT -- Toward a Realizability \u221e-Topos. (2017). Public lecture at the conference \"Big Proof","author":"Awodey Steve","unstructured":"Steve Awodey. 2017. Impredicative Encodings in HoTT -- Toward a Realizability \u221e-Topos. (2017). Public lecture at the conference \"Big Proof\", Newton Institute, Cambridge, available at https:\/\/www.newton.ac.uk\/files\/seminar\/20170711090010001-1009680.pdf."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.4.447"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Steve Awodey and Jonas Frey. 2018. Lean formalization of 'Impredicative encodings of (higher) inductive types'. (2018). https:\/\/github.com\/awodey\/Impredicative","DOI":"10.1145\/3209108.3209130"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3006383"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645735.666248"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/88278.88291"},{"key":"e_1_3_2_1_12_1","unstructured":"Nils Anders Danielsson. 2012. Positive h-levels are closed under W. (2012). https:\/\/homotopytypetheory.org\/2012\/09\/21\/positive-h-levels-are-closed-under-w"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120487"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"e_1_3_2_1_15_1","volume-title":"International Workshop on Types for Proofs and Programs. Springer, 210--225","author":"Gambino Nicola","year":"2003","unstructured":"Nicola Gambino and Martin Hyland. 2003. Wellfounded trees and dependent polynomial functors. In International Workshop on Types for Proofs and Programs. Springer, 210--225."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754639"},{"key":"e_1_3_2_1_17_1","unstructured":"Jean-Yves Girard. 1972. Interpretation Fonctionnelle et Elimination des Coupures de l'Arithm\u00e9tique d'Ordre Sup\u00e9rieur. Ph.D. Dissertation. Paris 7 France."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Jean-Yves Girard Paul Taylor and Yves Lafont. 1989. Proofs and Types. Cambridge University Press.","DOI":"10.5555\/64805"},{"key":"e_1_3_2_1_19_1","unstructured":"Martin Hofmann. 1995. Extensional concepts in intensional type theory. Ph.D. Dissertation. University of Edinburgh. College of Science and Engineering. School of Informatics."},{"key":"e_1_3_2_1_20_1","volume-title":"Twenty-five years of constructive type theory (Venice","author":"Hofmann Martin","year":"1995","unstructured":"Martin Hofmann and Thomas Streicher. 1998. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), Giovanni Sambin and Jan M. Smith (Eds.). Oxford Logic Guides, Vol. 36. Oxford University Press, New York, 83--111."},{"key":"e_1_3_2_1_21_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Roger Seldin, Jonathan P.","author":"Howard William A.","year":"1969","unstructured":"William A. Howard. 1980. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Roger Seldin, Jonathan P.; Hindley (Ed.). Academic Press, 479--490. original paper manuscript from 1969."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(81)90052-9"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.28"},{"key":"e_1_3_2_1_26_1","volume-title":"Studies in Proof Theory","volume":"1","author":"Martin-L\u00f6f Per","year":"1984","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in Proof Theory, Vol. 1. Bibliopolis. iv+91 pages. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00079-3"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645736.666272"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/648331.755423"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/647323.721503"},{"key":"e_1_3_2_1_31_1","volume-title":"Abstraction and Parametric Polymorphism. In IFIP Congress. 513--523","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress. 513--523."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_7"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.01.031"},{"key":"e_1_3_2_1_34_1","unstructured":"Mike Shulman. 2011. Higher Inductive Types via Impredicative Polymorphism. (2011). https:\/\/homotopytypetheory.org\/2011\/04\/25\/higher-inductive-types-via-impredicative-polymorphism\/"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676983"},{"key":"e_1_3_2_1_37_1","volume-title":"Impredicative Encodings of Inductive Types in Homotopy Type Theory. Master's thesis","author":"Speight Sam","unstructured":"Sam Speight. 2017. Impredicative Encodings of Inductive Types in Homotopy Type Theory. Master's thesis. Carnegie Mellon University, Pittsburgh, USA. https:\/\/github.com\/sspeight93\/Papers\/blob\/master\/impredicative-encodings-of-inductive-types-in-homotopy-type-theory.pdf"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"e_1_3_2_1_39_1","first-page":"78","article-title":"Universes in toposes. From Sets and Types to Topology and Analysis","volume":"48","author":"Thomas Streicher","year":"2005","unstructured":"Thomas Streicher et al. 2005. Universes in toposes. From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics 48 (2005), 78--90.","journal-title":"Towards Practicable Foundations for Constructive Mathematics"},{"key":"e_1_3_2_1_40_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","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_41_1","volume-title":"Predicative toposes. ArXiv e-prints (July","author":"van den Berg B.","year":"2012","unstructured":"B. van den Berg. 2012. Predicative toposes. ArXiv e-prints (July 2012). arXiv:math.CT\/1207.0959"}],"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","IEEE-CS\\DATC IEEE Computer Society","EACSL European Association for Computer Science Logic"]},"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.3209130","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209130","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209130","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:32:17Z","timestamp":1781854337000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":41,"alternative-id":["10.1145\/3209108.3209130","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209130","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}