{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:19Z","timestamp":1750220659262,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"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":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394771","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"88-101","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Algebraic models of simple type theories"],"prefix":"10.1145","author":[{"given":"Nathanael","family":"Arkor","sequence":"first","affiliation":[{"name":"Department of Computer Science and Technology, University of Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Fiore","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Technology, University of Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"volume-title":"Algebraic theories: A categorical introduction to general algebra","author":"Ad\u00e1mek Ji\u0159\u00ed","key":"e_1_3_2_1_2_1","unstructured":"Ji\u0159\u00ed Ad\u00e1mek , Ji\u0159\u00ed Rosick\u00fd , and Enrico Maria Vitale . 2010. Algebraic theories: A categorical introduction to general algebra . Vol. 184 . Cambridge University Press . Ji\u0159\u00ed Ad\u00e1mek, Ji\u0159\u00ed Rosick\u00fd, and Enrico Maria Vitale. 2010. Algebraic theories: A categorical introduction to general algebra. Vol. 184. Cambridge University Press."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_1_4_1","volume-title":"Polynomial pseudomonads and dependent type theory. arXiv preprint arXiv:1802.00997","author":"Awodey Steve","year":"2018","unstructured":"Steve Awodey and Clive Newstead . 2018. Polynomial pseudomonads and dependent type theory. arXiv preprint arXiv:1802.00997 ( 2018 ). Steve Awodey and Clive Newstead. 2018. Polynomial pseudomonads and dependent type theory. arXiv preprint arXiv:1802.00997 (2018)."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0021-9800(70)80014-X"},{"key":"e_1_3_2_1_6_1","volume-title":"arXiv preprint arXiv:1904.00827","author":"Castellan Simon","year":"2019","unstructured":"Simon Castellan , Pierre Clairambault , and Peter Dybjer . 2019. Categories with Families: Unityped , Simply Typed, and Dependently Typed. arXiv preprint arXiv:1904.00827 ( 2019 ). Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2019. Categories with Families: Unityped, Simply Typed, and Dependently Typed. arXiv preprint arXiv:1904.00827 (2019)."},{"volume-title":"Categories for types","author":"Crole Roy L","key":"e_1_3_2_1_7_1","unstructured":"Roy L Crole . 1993. Categories for types . Cambridge University Press . Roy L Crole. 1993. Categories for types. Cambridge University Press."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_10_1","unstructured":"Marcelo Fiore. 2008. Algebraic Type Theory. (2008). https:\/\/www.cl.cam.ac.uk\/~mpf23\/Notes\/att.pdf Unpublished (Accessed 2020-05-01).  Marcelo Fiore. 2008. Algebraic Type Theory. (2008). https:\/\/www.cl.cam.ac.uk\/~mpf23\/Notes\/att.pdf Unpublished (Accessed 2020-05-01)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.38"},{"volume-title":"Algebraic Foundations for Type Theories. (2011). https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/Types2011.pdf Talk given at the 18th Workshop of Types for Proofs and Programs (Accessed 2020-05-01)","author":"Fiore Marcelo","key":"e_1_3_2_1_12_1","unstructured":"Marcelo Fiore . 2011. Algebraic Foundations for Type Theories. (2011). https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/Types2011.pdf Talk given at the 18th Workshop of Types for Proofs and Programs (Accessed 2020-05-01) . Marcelo Fiore. 2011. Algebraic Foundations for Type Theories. (2011). https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/Types2011.pdf Talk given at the 18th Workshop of Types for Proofs and Programs (Accessed 2020-05-01)."},{"volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Fiore Marcelo","key":"e_1_3_2_1_13_1","unstructured":"Marcelo Fiore . 2012. Discrete generalised polynomial functors . In International Colloquium on Automata, Languages, and Programming . Springer , 214--226. Marcelo Fiore. 2012. Discrete generalised polynomial functors. In International Colloquium on Automata, Languages, and Programming. Springer, 214--226."},{"key":"e_1_3_2_1_14_1","unstructured":"Marcelo Fiore. 2012. Discrete generalised polynomial functors. (2012). http:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/ICALP2012.pdf Talk presented at ICALP 2012 (Accessed 2020-05-01).  Marcelo Fiore. 2012. Discrete generalised polynomial functors. (2012). http:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/ICALP2012.pdf Talk presented at ICALP 2012 (Accessed 2020-05-01)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.59"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.12.052"},{"key":"e_1_3_2_1_17_1","volume-title":"International Workshop on Computer Science Logic. Springer, 320--335","author":"Fiore Marcelo","year":"2010","unstructured":"Marcelo Fiore and Chung-Kil Hur . 2010 . Second-order equational logic . In International Workshop on Computer Science Logic. Springer, 320--335 . Marcelo Fiore and Chung-Kil Hur. 2010. Second-order equational logic. In International Workshop on Computer Science Logic. Springer, 320--335."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603163"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"e_1_3_2_1_21_1","unstructured":"J.A. Goguen J.W. Thatcher and E.G. Wagner. 1976. An Initial Algebra Approach to the Specification Correctness and Implementation of Abstract Data Types. IBM Thomas J. Watson Research Division.  J.A. Goguen J.W. Thatcher and E.G. Wagner. 1976. An Initial Algebra Approach to the Specification Correctness and Implementation of Abstract Data Types. IBM Thomas J. Watson Research Division."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_23"},{"key":"e_1_3_2_1_23_1","volume-title":"From Lambda-calculus to Cartesian Closed Categories. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Lambek Joachim","year":"1980","unstructured":"Joachim Lambek . 1980. From Lambda-calculus to Cartesian Closed Categories. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism ( 1980 ), 376--402. Joachim Lambek. 1980. From Lambda-calculus to Cartesian Closed Categories. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), 376--402."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f Per","key":"e_1_3_2_1_25_1","unstructured":"Per Martin-L\u00f6f . 1984. Intuitionistic type theory . Vol. 9 . Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Vol. 9."},{"key":"e_1_3_2_1_26_1","volume-title":"Notions of computation and monads. Information and computation 93, 1","author":"Moggi Eugenio","year":"1991","unstructured":"Eugenio Moggi . 1991. Notions of computation and monads. Information and computation 93, 1 ( 1991 ), 55--92. Eugenio Moggi. 1991. Notions of computation and monads. Information and computation 93, 1 (1991), 55--92."},{"key":"e_1_3_2_1_28_1","first-page":"533","article-title":"Polynomials in categories with pullbacks","volume":"30","author":"Weber Mark","year":"2015","unstructured":"Mark Weber . 2015 . Polynomials in categories with pullbacks . Theory and Applications of Categories 30 , 15 (2015), 533 -- 598 . Mark Weber. 2015. Polynomials in categories with pullbacks. Theory and Applications of Categories 30, 15 (2015), 533--598.","journal-title":"Theory and Applications of Categories"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"Saarbr\u00fccken Germany","acronym":"LICS '20"},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394771","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394771"}},"subtitle":["A polynomial approach"],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":27,"alternative-id":["10.1145\/3373718.3394771","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394771","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}