{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:10Z","timestamp":1750307710789,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"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":[[2009,1,20]]},"DOI":"10.1145\/1481848.1481857","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"59-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Embedding a logical theory of constructions in Agda"],"prefix":"10.1145","author":[{"given":"Ana","family":"Bove","sequence":"first","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9s","family":"Sicard-Ram\u00edrez","sequence":"additional","affiliation":[{"name":"EAFIT University, Medell\u00edn, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088355"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_17"},{"key":"e_1_3_2_1_3_1","first-page":"122","volume-title":"Proc. of the Worshop on Programming Logic, number 54 in Programming Methodology Group Reports","author":"Aczel Peter","year":"1989"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Peter\n       \n      Aczel\n    .\n      \n  \n   \n  Frege structures and the notion of proposition truth and set. In J. Barwise H. J. Keisler and K. Kunen editors The Kleene Symposium volume \n  101\n   of \n  Studies in Logic and the Foundations of Mathematics pages \n  31\n  --\n  59\n  . \n  Amsterdan\n  : \n  North-Holland 1980\n  .  Peter Aczel. Frege structures and the notion of proposition truth and set. In J. Barwise H. J. Keisler and K. Kunen editors The Kleene Symposium volume 101 of Studies in Logic and the Foundations of Mathematics pages 31--59. Amsterdan: North-Holland 1980.","DOI":"10.1016\/S0049-237X(08)71252-7"},{"volume-title":"Proc. of the Symposium on Mathematical Logic (Oulu, 1974","year":"1977","author":"Aczel Peter","key":"e_1_3_2_1_5_1"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120478"},{"key":"e_1_3_2_1_7_1","unstructured":"Agda wiki. Available at appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php 2008.  Agda wiki. Available at appserv.cs.chalmers.se\/users\/ulfn\/wiki\/agda.php 2008."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Ana Bove and Peter Dybjer. Dependent types at work 2008. Lecture notes of a graduate course with the same name. Submitted for publication in the post-proceedings of the International Summer School on Language Engineering and Rigorous Software Development.  Ana Bove and Peter Dybjer. Dependent types at work 2008. Lecture notes of a graduate course with the same name. Submitted for publication in the post-proceedings of the International Summer School on Language Engineering and Rigorous Software Development.","DOI":"10.1007\/978-3-642-03153-3_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351266"},{"key":"e_1_3_2_1_12_1","first-page":"55","volume-title":"Implementation of Functional Languages. 13th International Workshop, IFL 2001","volume":"2312","author":"de Mol Maarten","year":"2002"},{"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","series-title":"LNCS","first-page":"334","volume-title":"J.-P","author":"Dybjer Peter","year":"1985"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90058-L"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887211"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(95)00028-3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Jean-Yves\n       \n      Girard\n    .\n      \n  \n   \n  Linear logic and parallelism. In M. Venturini Zilli editor Mathematical Models for the Semantics of Parallelism volume \n  280\n   of \n  LNCS pages \n  166\n  --\n  182 1986\n  .   Jean-Yves Girard. Linear logic and parallelism. In M. Venturini Zilli editor Mathematical Models for the Semantics of Parallelism volume 280 of LNCS pages 166--182 1986.","DOI":"10.1007\/3-540-18419-8_14"},{"volume-title":"Department of Computer Science and Engineering","year":"2006","author":"Gonzal\u00eda Carlos","key":"e_1_3_2_1_19_1"},{"key":"e_1_3_2_1_20_1","unstructured":"Michael J. C.\n       \n      Gordon Robin\n       \n      Milner and \n      \n      \n      Christopher P.\n       \n      Wadsworth\n      \n  \n  . \n  Edinburgh LCF volume \n  78\n   of \n  Lecture Notes in Computer Science\n  . \n  Springer-Verlag 1979\n  .  Michael J. C. Gordon Robin Milner and Christopher P. Wadsworth. Edinburgh LCF volume 78 of Lecture Notes in Computer Science. Springer-Verlag 1979."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005666"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00252182"},{"volume-title":"Department of Computer Science and Engineering","year":"2007","author":"Norell Ulf","key":"e_1_3_2_1_24_1"},{"key":"e_1_3_2_1_25_1","unstructured":"Lawrence C.\n       \n      Paulson\n    . Isabelle.\n      \n  \n   \n  A Generic Theorem Prover volume \n  828\n   of \n  LNCS\n  . \n  Springer 1994\n  . (With a contribution by T. Nipkow). Simon Peyton Jones editor. Haskell 98 Language and Libraries The Revised Report. Cambridge University Press April 2003.  Lawrence C. Paulson. Isabelle. A Generic Theorem Prover volume 828 of LNCS. Springer 1994. (With a contribution by T. Nipkow). Simon Peyton Jones editor. Haskell 98 Language and Libraries The Revised Report. Cambridge University Press April 2003."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274128"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Savannah GA USA","acronym":"POPL09"},"container-title":["Proceedings of the 3rd workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481857","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481848.1481857","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481848.1481857"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":28,"alternative-id":["10.1145\/1481848.1481857","10.1145\/1481848"],"URL":"https:\/\/doi.org\/10.1145\/1481848.1481857","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}