{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:54Z","timestamp":1774837854114,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,9,27]],"date-time":"2010-09-27T00:00:00Z","timestamp":1285545600000},"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":[[2010,9,27]]},"DOI":"10.1145\/1863543.1863591","type":"proceedings-article","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T13:41:50Z","timestamp":1285681310000},"page":"333-344","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["VeriML"],"prefix":"10.1145","author":[{"given":"Antonis","family":"Stampoulis","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT, USA"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}]}],"member":"320","published-online":{"date-parts":[[2010,9,27]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Handbook of Automated Reasoning","author":"Henk","year":"1999","unstructured":"}} Henk P. Barendregt and Herman Geuvers. Proof-assistants using dependent type systems . In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning . Elsevier Sci . Pub. B.V., 1999 . }}Henk P. Barendregt and Herman Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Sci. Pub. B.V., 1999."},{"key":"e_1_3_2_2_2_1","volume-title":"The Coq proof assistant reference manual (version 8.3)","author":"Barras B.","year":"2010","unstructured":"}} B. Barras , S. Boutin , C. Cornes , J. Courant , Y. Coscoy , D. Delahaye , D. de Rauglaudre , J.C. Filli\u00e2tre , E. Gim\u00e9nez , H. Herbelin , The Coq proof assistant reference manual (version 8.3) , 2010 . }}B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, et al. The Coq proof assistant reference manual (version 8.3), 2010."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/645869.668533"},{"key":"e_1_3_2_2_4_1","volume-title":"The calculus of computation: decision procedures with applications to verification","author":"Bradley A. R.","year":"2007","unstructured":"}} A. R. Bradley and Z. Manna . The calculus of computation: decision procedures with applications to verification . Springer-Verlag New York Inc , 2007 . }}A. R. Bradley and Z. Manna. The calculus of computation: decision procedures with applications to verification. Springer-Verlag New York Inc, 2007."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_2_6_1","volume-title":"Certified Programming with Dependent Types","author":"Chlipala A.","year":"2008","unstructured":"}} A. Chlipala . Certified Programming with Dependent Types , 2008 . URL http:\/\/adam.chlipala.net\/cpdt. }}A. Chlipala. Certified Programming with Dependent Types, 2008. URL http:\/\/adam.chlipala.net\/cpdt."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_2_8_1","first-page":"85","volume-title":"A tactic language for the system Coq. Lecture notes in computer science","author":"Delahaye D.","year":"2000","unstructured":"}} D. Delahaye . A tactic language for the system Coq. Lecture notes in computer science , pages 85 -- 95 , 2000 . }}D. Delahaye. A tactic language for the system Coq. Lecture notes in computer science, pages 85--95, 2000."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80508-5"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_8"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_3_2_2_12_1","first-page":"11","article-title":"Edinburgh LCF: a mechanized logic of computation","volume":"10","author":"Gordon M. J.","year":"1979","unstructured":"}} M. J. Gordon , R. Milner , and C.P. Wadsworth . Edinburgh LCF: a mechanized logic of computation . Springer-Verlag Berlin , 10 : 11 -- 25 , 1979 . }}M. J. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF: a mechanized logic of computation. Springer-Verlag Berlin, 10: 11--25, 1979.","journal-title":"Springer-Verlag Berlin"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_2_14_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"HOL Light: A tutorial introduction","author":"Harrison J.","year":"1996","unstructured":"}} J. Harrison . HOL Light: A tutorial introduction . Lecture Notes in Computer Science , pages 265 -- 269 , 1996 . }}J. Harrison. HOL Light: A tutorial introduction. Lecture Notes in Computer Science, pages 265--269, 1996."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480935"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.48"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_3_2_2_22_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL : A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"}} T. Nipkow , L.C. Paulson , and M. Wenzel . Isabelle\/HOL : A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS , 2002 . }}T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS, 2002."},{"key":"e_1_3_2_2_23_1","volume-title":"Towards a practical programming language based on dependent type theory. Technical report","author":"Norell Ulf","year":"2007","unstructured":"}} Ulf Norell . Towards a practical programming language based on dependent type theory. Technical report , Goteborg University , 2007 . }}Ulf Norell. Towards a practical programming language based on dependent type theory. Technical report, Goteborg University, 2007."},{"key":"e_1_3_2_2_24_1","first-page":"328","volume-title":"Lecture Notes in Computer Science","author":"Paulin-Mohring C.","year":"1993","unstructured":"}} C. Paulin-Mohring . Inductive definitions in the system Coq; rules and properties . Lecture Notes in Computer Science , pages 328 -- 328 , 1993 . }}C. Paulin-Mohring. Inductive definitions in the system Coq; rules and properties. Lecture Notes in Computer Science, pages 328--328, 1993."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_3_2_2_27_1","volume-title":"Types and programming languages","author":"Pierce B.C.","year":"2002","unstructured":"}} B.C. Pierce . Types and programming languages . The MIT Press , 2002 . }}B.C. Pierce. Types and programming languages. The MIT Press, 2002."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792887"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"e_1_3_2_2_31_1","volume-title":"Dept. of Computer Science","author":"Stampoulis A.","year":"2010","unstructured":"}} A. Stampoulis and Z. Shao . VeriML: Typed computation of logical terms inside a language with effects (extended version). Technical report YALEU\/DCS\/TR-1430 , Dept. of Computer Science , Yale University , New Haven, CT , 2010 . URL http:\/\/flint.cs.yale.edu\/publications\/veriml.htm. }}A. Stampoulis and Z. Shao. VeriML: Typed computation of logical terms inside a language with effects (extended version). Technical report YALEU\/DCS\/TR-1430, Dept. of Computer Science, Yale University, New Haven, CT, 2010. URL http:\/\/flint.cs.yale.edu\/publications\/veriml.htm."},{"key":"e_1_3_2_2_32_1","volume-title":"Studies in constructive mathematics and mathematical logic. 2 (115--125): 10--13","author":"Tseitin G.S.","year":"1968","unstructured":"}} G.S. Tseitin . On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic. 2 (115--125): 10--13 , 1968 . }}G.S. Tseitin. On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic. 2 (115--125): 10--13, 1968."}],"event":{"name":"ICFP '10: ACM SIGPLAN International Conference on Functional Programming","location":"Baltimore Maryland USA","acronym":"ICFP '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 15th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863591","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1863543.1863591","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:39:52Z","timestamp":1750232392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1863543.1863591"}},"subtitle":["typed computation of logical terms inside a language with effects"],"short-title":[],"issued":{"date-parts":[[2010,9,27]]},"references-count":32,"alternative-id":["10.1145\/1863543.1863591","10.1145\/1863543"],"URL":"https:\/\/doi.org\/10.1145\/1863543.1863591","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1932681.1863591","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,9,27]]},"assertion":[{"value":"2010-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}