{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:00Z","timestamp":1751660520506,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"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"}],"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.3209153","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"879-888","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Guarded Computational Type Theory"],"prefix":"10.1145","author":[{"given":"Jonathan","family":"Sterling","sequence":"first","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"e_1_3_2_1_4_1","volume-title":"Interactive Theorem Proving: 5th International Conference, ITP","author":"Anand Abhishek","year":"2014","unstructured":"Abhishek Anand and Vincent Rahli . 2014. Towards a Formally Verified Proof Assistant . In Interactive Theorem Proving: 5th International Conference, ITP 2014 , Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing , Cham, 27--44. Abhishek Anand and Vincent Rahli. 2014. Towards a Formally Verified Proof Assistant. In Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing, Cham, 27--44."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500597"},{"volume-title":"2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1--12","author":"Bahr P.","key":"e_1_3_2_1_7_1","unstructured":"P. Bahr , H. B. Grathwohl , and R. E. M\u00f8gelberg . 2017. The clocks are ticking: No more delays! . In 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1--12 . P. Bahr, H. B. Grathwohl, and R. E. M\u00f8gelberg. 2017. The clocks are ticking: No more delays!. In 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1--12."},{"key":"e_1_3_2_1_8_1","volume-title":"Bas Spitters, and Andrea Vezzosi.","author":"Birkedal Lars","year":"2016","unstructured":"Lars Birkedal , Ale\u0161 Bizjak , Ranald Clouston , Hans Bugge Grathwohl , Bas Spitters, and Andrea Vezzosi. 2016 . Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 23:1--23:17. Lars Birkedal, Ale\u0161 Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2016. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016) (Leibniz International Proceedings in Informatics (LIPIcs)), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 23:1--23:17."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"volume-title":"A Model of Countable Nondeterminism in Guarded Type Theory","author":"Bizjak Ale\u0161","key":"e_1_3_2_1_11_1","unstructured":"Ale\u0161 Bizjak , Lars Birkedal , and Marino Miculan . 2014. A Model of Countable Nondeterminism in Guarded Type Theory . In Rewriting and Typed Lambda Calculi, Gilles Dowek (Ed.). Springer International Publishing , Cham , 108--123. Ale\u0161 Bizjak, Lars Birkedal, and Marino Miculan. 2014. A Model of Countable Nondeterminism in Guarded Type Theory. In Rewriting and Typed Lambda Calculi, Gilles Dowek (Ed.). Springer International Publishing, Cham, 108--123."},{"key":"e_1_3_2_1_12_1","volume-title":"Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal.","author":"Bizjak Ale\u0161","year":"2016","unstructured":"Ale\u0161 Bizjak , Hans Bugge Grathwohl , Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal. 2016 . Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 20--35. Ale\u0161 Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 20--35."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.007"},{"key":"e_1_3_2_1_14_1","unstructured":"Ale\u0161 Bizjak and Rasmus Ejlers M\u00f8gelberg. 2017. Denotational semantics for guarded dependent type theory. (2017). Draft.  Ale\u0161 Bizjak and Rasmus Ejlers M\u00f8gelberg. 2017. Denotational semantics for guarded dependent type theory. (2017). Draft."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"volume-title":"Brouwer's Cambridge Lectures on Intuitionism","author":"Brouwer L. E. J.","key":"e_1_3_2_1_16_1","unstructured":"L. E. J. Brouwer . 1981. Brouwer's Cambridge Lectures on Intuitionism . Cambridge University Press . L. E. J. Brouwer. 1981. Brouwer's Cambridge Lectures on Intuitionism. Cambridge University Press."},{"key":"e_1_3_2_1_17_1","volume-title":"Andrew M. Pitts, and Bas Spitters.","author":"Clouston Ranald","year":"2018","unstructured":"Ranald Clouston , Bassel Mannaa , Rasmus Ejlers M\u00f8gelberg , Andrew M. Pitts, and Bas Spitters. 2018 . Modal Dependent Type Theory and Dependent Right Adjoints . (2018). https:\/\/arxiv.org\/abs\/1804.05236. Ranald Clouston, Bassel Mannaa, Rasmus Ejlers M\u00f8gelberg, Andrew M. Pitts, and Bas Spitters. 2018. Modal Dependent Type Theory and Dependent Right Adjoints. (2018). https:\/\/arxiv.org\/abs\/1804.05236."},{"key":"e_1_3_2_1_18_1","unstructured":"R. L. Constable S. F. Allen H. M. Bromley W. R. Cleaveland J. F. Cremer R. W. Harper D. J. Howe T. B. Knoblock N. P. Mendler P. Panangaden J. T. Sasaki and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc. Upper Saddle River NJ USA.   R. L. Constable S. F. Allen H. M. Bromley W. R. Cleaveland J. F. Cremer R. W. Harper D. J. Howe T. B. Knoblock N. P. Mendler P. Panangaden J. T. Sasaki and S. F. Smith. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc. Upper Saddle River NJ USA."},{"volume-title":"Categories for Types","author":"Crole R.L.","key":"e_1_3_2_1_20_1","unstructured":"R.L. Crole . 1993. Categories for Types . Cambridge University Press , New York . R.L. Crole. 1993. Categories for Types. Cambridge University Press, New York."},{"key":"e_1_3_2_1_21_1","volume-title":"Priestley","author":"Davey Brian A.","year":"1990","unstructured":"Brian A. Davey and Hilary A . Priestley . 1990 . Introduction to lattices and order. Cambridge University Press , Cambridge. Brian A. Davey and Hilary A. Priestley. 1990. Introduction to lattices and order. Cambridge University Press, Cambridge."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_11"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77371"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"volume-title":"Sheaves in geometry and logic: a first introduction to topos theory","author":"Lane Saunders Mac","key":"e_1_3_2_1_25_1","unstructured":"Saunders Mac Lane and Ieke Moerdijk . 1992. Sheaves in geometry and logic: a first introduction to topos theory . Springer , New York . Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in geometry and logic: a first introduction to topos theory. Springer, New York."},{"key":"e_1_3_2_1_26_1","volume-title":"Constructive Mathematics and Computer Programming. In 6th International Congress for Logic, Methodology and Philosophy of Science. Hanover, 153--175","author":"Martin-L\u00f6f Per","year":"1979","unstructured":"Per Martin-L\u00f6f . 1979 . Constructive Mathematics and Computer Programming. In 6th International Congress for Logic, Methodology and Philosophy of Science. Hanover, 153--175 . Published by North Holland, Amsterdam. 1982. Per Martin-L\u00f6f. 1979. Constructive Mathematics and Computer Programming. In 6th International Congress for Logic, Methodology and Philosophy of Science. Hanover, 153--175. Published by North Holland, Amsterdam. 1982."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00012-9"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.020"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005074"},{"key":"e_1_3_2_1_33_1","volume-title":"echnical Report).","author":"Sterling Jonathan","year":"2018","unstructured":"Jonathan Sterling and Robert Harper . 2018. Guarded Computational Type Theory ( T echnical Report). ( 2018 ). https:\/\/arxiv.org\/abs\/1804.09098 Jonathan Sterling and Robert Harper. 2018. Guarded Computational Type Theory (Technical Report). (2018). https:\/\/arxiv.org\/abs\/1804.09098"},{"key":"e_1_3_2_1_34_1","unstructured":"Jonathan Sterling and Robert Harper. 2018. coq-guarded-type-theory. (2018). https:\/\/github.com\/jonsterling\/coq-guarded-type-theory  Jonathan Sterling and Robert Harper. 2018. coq-guarded-type-theory. (2018). https:\/\/github.com\/jonsterling\/coq-guarded-type-theory"},{"key":"e_1_3_2_1_35_1","unstructured":"The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual. (2016).  The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual. (2016)."},{"key":"e_1_3_2_1_36_1","unstructured":"Andrea Vezzosi. 2015. Guarded Recursive Types in Type Theory. Institutionen f\u00f6r data- och informationsteknik Datavetenskap (Chalmers) Chalmers tekniska h\u00f6gskola. 63.  Andrea Vezzosi. 2015. Guarded Recursive Types in Type Theory. Institutionen f\u00f6r data- och informationsteknik Datavetenskap (Chalmers) Chalmers tekniska h\u00f6gskola. 63."}],"event":{"name":"LICS '18: 33rd 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":"Oxford United Kingdom","acronym":"LICS '18"},"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.3209153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209153","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:07Z","timestamp":1750212427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":32,"alternative-id":["10.1145\/3209108.3209153","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209153","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"}}]}}