{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:45:25Z","timestamp":1772163925377,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,9,12]],"date-time":"2005-09-12T00:00:00Z","timestamp":1126483200000},"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":[[2005,9,12]]},"DOI":"10.1145\/1086365.1086375","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T12:34:39Z","timestamp":1131366879000},"page":"66-77","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":68,"title":["Combining programming with theorem proving"],"prefix":"10.1145","author":[{"given":"Chiyan","family":"Chen","sequence":"first","affiliation":[{"name":"Boston University"}]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[{"name":"Boston University"}]}],"member":"320","published-online":{"date-parts":[[2005,9,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"November","author":"CHEN C.","year":"2004","unstructured":"CHEN , C. , AND XI , H. Combining Programming with Theorem Proving , November 2004 . Available at: http:\/\/www.cs.bu.edu ~hwxi\/ATS\/PAPER\/CPwTP.ps.]] CHEN, C., AND XI, H. Combining Programming with Theorem Proving, November 2004. Available at: http:\/\/www.cs.bu.edu ~hwxi\/ATS\/PAPER\/CPwTP.ps.]]"},{"key":"e_1_3_2_1_2_1","volume-title":"H. Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages","volume":"3057","author":"CHEN C.","year":"2004","unstructured":"CHEN , C. , ZHU , D. , AND XI , H. Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages ( Dallas, TX , June 2004 ), Springer-Verlag LNCS vol. 3057 .]] CHEN, C., ZHU, D., AND XI, H. Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages (Dallas, TX, June 2004), Springer-Verlag LNCS vol. 3057.]]"},{"key":"e_1_3_2_1_3_1","volume-title":"Technical Report CUCIS-TR2003-1901","author":"CHENEY J.","year":"2003","unstructured":"CHENEY , J. , AND HINZE , R. Phantom Types. Technical Report CUCIS-TR2003-1901 , Cornell University , 2003 . Available at http:\/\/techreports.library.cornell.edu:8081\/Dienst\/UI\/1.0\/Display\/cul.cis\/TR2003-1901.]] CHENEY, J., AND HINZE, R. Phantom Types. Technical Report CUCIS-TR2003-1901, Cornell University, 2003. Available at http:\/\/techreports.library.cornell.edu:8081\/Dienst\/UI\/1.0\/Display\/cul.cis\/TR2003-1901.]]"},{"key":"e_1_3_2_1_4_1","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"CONSTABLE R. L.","year":"1986","unstructured":"CONSTABLE , R. L. , ET AL . Implementing Mathematics with the NuPrl Proof Development System . Prentice-Hall , Englewood Cliffs , New Jersey, 1986 .]] CONSTABLE, R. L., ET AL. Implementing Mathematics with the NuPrl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.]]"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"e_1_3_2_1_7_1","volume-title":"INRIA","author":"DOWEK G.","year":"1993","unstructured":"DOWEK , G. , FELTY , A. , HERBELIN , H. , HUET , G. , MURTHY , C. , PARENT , C. , PAULIN-MOHRING , C. , AND WERNER , B. The Coq proof assistant user's guide. Rapport Technique 154 , INRIA , Rocquencourt, France , 1993 . Version 5.8.]] DOWEK, G., FELTY, A., HERBELIN, H., HUET, G., MURTHY, C., PARENT, C., PAULIN-MOHRING, C., AND WERNER, B. The Coq proof assistant user's guide. Rapport Technique 154, INRIA, Rocquencourt, France, 1993. Version 5.8.]]"},{"key":"e_1_3_2_1_9_1","volume-title":"Bibliopolis","author":"MARTIN-L\u00d6F P.","year":"1984","unstructured":"MARTIN-L\u00d6F , P. Intuitionistic Type Theory . Bibliopolis , Naples, Italy , 1984 .]] MARTIN-L\u00d6F, P. Intuitionistic Type Theory. Bibliopolis, Naples, Italy, 1984.]]"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004355"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/549659"},{"key":"e_1_3_2_1_13_1","series-title":"International Series of Monographs on Computer Science","volume-title":"Programming in Martin-L\u00f6f's Type Theory","author":"NORDSTR\u00d6M B.","year":"1990","unstructured":"NORDSTR\u00d6M , B. , PETERSSON , K. , AND SMITH , J. M. Programming in Martin-L\u00f6f's Type Theory , vol. 7 of International Series of Monographs on Computer Science . Clarendon Press , Oxford , 1990 .]] NORDSTR\u00d6M, B., PETERSSON, K., AND SMITH, J. M. Programming in Martin-L\u00f6f's Type Theory, vol. 7 of International Series of Monographs on Computer Science. Clarendon Press, Oxford, 1990.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"Universit\u00e9 de Paris VII","author":"PAULIN-MOHRING C.","year":"1989","unstructured":"PAULIN-MOHRING , C. Extraction de programmes dans le Calcul des Constructions. Th\u00e8se de doctorat d'\u00e9tat , Universit\u00e9 de Paris VII , Paris, France , 1989 .]] PAULIN-MOHRING, C. Extraction de programmes dans le Calcul des Constructions. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 de Paris VII, Paris, France, 1989.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"C. Inductive Definitions in the System Coq: Rules and Properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications","author":"PAULIN-MOHRING","year":"1993","unstructured":"PAULIN-MOHRING , C. Inductive Definitions in the System Coq: Rules and Properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications ( Utrecht, The Netherlands , 1993 ), M. Bezem and J. de Groote, Eds., vol. 664 of Lecture Notes in Computer Science, pp. 328--345.]] PAULIN-MOHRING, C. Inductive Definitions in the System Coq: Rules and Properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (Utrecht, The Netherlands, 1993), M. Bezem and J. de Groote, Eds., vol. 664 of Lecture Notes in Computer Science, pp. 328--345.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503293"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1028664.1028711"},{"key":"e_1_3_2_1_20_1","volume-title":"The First International Workshop on Practical Aspects of Declarative Languages (San Antonio","volume":"1551","author":"XI H.","year":"1999","unstructured":"XI , H. Dead code elimination through dependent types . In The First International Workshop on Practical Aspects of Declarative Languages (San Antonio , January 1999 ), Springer-Verlag LNCS vol. 1551 .]] XI, H. Dead code elimination through dependent types. In The First International Workshop on Practical Aspects of Declarative Languages (San Antonio, January 1999), Springer-Verlag LNCS vol. 1551.]]"},{"key":"e_1_3_2_1_21_1","unstructured":"XI H.\n     Dependent     \n      ML.\n   Available at http:\/\/www.cs.bu.edu\/~hwxi\/DML\/DML.html 2001\n  .]]  XI H. Dependent ML. Available at http:\/\/www.cs.bu.edu\/~hwxi\/DML\/DML.html 2001.]]"},{"key":"e_1_3_2_1_22_1","first-page":"231","volume-title":"H. Dependent Types for Program Termination Verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science","author":"XI","year":"2001","unstructured":"XI , H. Dependent Types for Program Termination Verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science ( Boston , June 2001 ), pp. 231 -- 242 .]] XI, H. Dependent Types for Program Termination Verification. In Proceedings of 16th IEEE Symposium on Logic in Computer Science (Boston, June 2001), pp. 231--242.]]"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"},{"key":"e_1_3_2_1_24_1","first-page":"8","article-title":"Dependently Typed Pattern Matching","volume":"9","author":"XI H","year":"2003","unstructured":"XI , H . Dependently Typed Pattern Matching . Journal of Universal Computer Science 9 , 8 ( 2003 ), 851--872.]] XI, H. Dependently Typed Pattern Matching. Journal of Universal Computer Science 9, 8 (2003), 851--872.]]","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_1_25_1","first-page":"394","volume-title":"Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003","author":"XI H.","year":"2004","unstructured":"XI , H. Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003 ( 2004 ), Springer-Verlag LNCS 3085, pp. 394 -- 408 .]] XI, H. Applied Type System (extended abstract). In post-workshop Proceedings of TYPES 2003 (2004), Springer-Verlag LNCS 3085, pp. 394--408.]]"},{"key":"e_1_3_2_1_26_1","volume-title":"September","author":"XI H.","year":"2004","unstructured":"XI , H. Dependent Types for Practical Programming via Applied Type System , September 2004 . Available at http:\/\/www.cs.bu.edu\/~hwxi\/academic\/drafts\/ATSdml.ps]] XI, H. Dependent Types for Practical Programming via Applied Type System, September 2004. Available at http:\/\/www.cs.bu.edu\/~hwxi\/academic\/drafts\/ATSdml.ps]]"},{"key":"e_1_3_2_1_27_1","volume-title":"Applied Type System","author":"XI H.","year":"2005","unstructured":"XI , H. Applied Type System , 2005 . Available at: http:\/\/www.cs.bu.edu\/~hwxi\/ATS.]] XI, H. Applied Type System, 2005. Available at: http:\/\/www.cs.bu.edu\/~hwxi\/ATS.]]"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_2_1_29_1","unstructured":"XI H. AND ZHU D. Views Types and Viewtypes October 2004. Available at: http:\/\/www.cs.bu.edu\/~hwxi\/ATS\/PAPER\/VsTsVTs.ps.]]  XI H. AND ZHU D. Views Types and Viewtypes October 2004. Available at: http:\/\/www.cs.bu.edu\/~hwxi\/ATS\/PAPER\/VsTsVTs.ps.]]"}],"event":{"name":"ICFP05: ACM SIGPLAN International Conference on Functional Programming","location":"Tallinn Estonia","acronym":"ICFP05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the tenth ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1086365.1086375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:12Z","timestamp":1750248492000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,12]]},"references-count":28,"alternative-id":["10.1145\/1086365.1086375","10.1145\/1086365"],"URL":"https:\/\/doi.org\/10.1145\/1086365.1086375","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1090189.1086375","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,9,12]]},"assertion":[{"value":"2005-09-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}