{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T18:24:24Z","timestamp":1729621464499,"version":"3.28.0"},"reference-count":31,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1109\/sefm.2003.1236209","type":"proceedings-article","created":{"date-parts":[[2004,1,24]],"date-time":"2004-01-24T04:33:03Z","timestamp":1074918783000},"page":"72-81","source":"Crossref","is-referenced-by-count":0,"title":["Facilitating program verification with dependent types"],"prefix":"10.1109","author":[{"family":"Hongwei Xi","sequence":"first","affiliation":[]}],"member":"263","reference":[{"journal-title":"Indizierte Typen","year":"1998","author":"zenger","key":"ref31"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00062-5"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1077"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"journal-title":"INRIA Caml-light","year":"0","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663086"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054269"},{"journal-title":"Intuitionistic type theory","year":"1984","author":"martin-l\u00f6f","key":"ref16"},{"key":"ref17","first-page":"30","article-title":"Recursive types and type constraints in second-order lambda calculus","author":"mendler","year":"1987","journal-title":"Proc Symp Logic Comput Sci"},{"key":"ref18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","author":"milner","year":"1997","journal-title":"The Definition of Standard ML (Revised)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90087-6"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"ref4","first-page":"183","article-title":"Partial objects in constructive type theory","author":"constable","year":"1987","journal-title":"Proc Symp Logic Comput Sci"},{"key":"ref27","article-title":"A Dependently Typed Assembly Language","author":"xi","year":"1999","journal-title":"Technical Report CSE-99-008 Oregon Graduate Institute"},{"journal-title":"Implementing Mathematics with the Nuprl Proof Development System","year":"1986","author":"constable","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"ref5","article-title":"An overview of the extended static checking system","author":"detlefs","year":"1996","journal-title":"Second Workshop on Formal Methods in Software Practice"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"ref7","article-title":"The Coq proof assistant user's guide","author":"dowek","year":"1993","journal-title":"Rapport Technique 154 INRIA"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"journal-title":"The Java Programming Language","year":"1997","author":"arnold","key":"ref1"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","article-title":"PVS: Combining specification, proof checking, and model checking","volume":"1102","author":"owre","year":"1996","journal-title":"Proceedings of the 8th International Conference on Computer-Aided Verification (CAV '96)"},{"journal-title":"Le Langage Caml InterEditions","year":"1993","author":"weis","key":"ref22"},{"article-title":"Practical refinement-type checking","year":"1997","author":"rowan","key":"ref21"},{"key":"ref24","first-page":"375","article-title":"Imperative Programming with Dependent Types","author":"xi","year":"2000","journal-title":"Proceedings of the IEEE Symposium on Logic in Computer Science"},{"journal-title":"Dependent Types in Practical Programming","year":"1998","author":"xi","key":"ref23"},{"article-title":"Xanadu: Imperative Programming with Dependent Types","year":"2001","author":"xi","key":"ref26"},{"year":"2001","author":"xi","key":"ref25"}],"event":{"name":"1st IEEE International Conference Software Engineering and Formal Methods. SEFM'03","start":{"date-parts":[[2003,9,22]]},"location":"Brisbane, Queensland, Australia","end":{"date-parts":[[2003,9,27]]}},"container-title":["First International Conference onSoftware Engineering and Formal Methods, 2003.Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8747\/27706\/01236209.pdf?arnumber=1236209","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T08:01:15Z","timestamp":1585468875000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1236209\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/sefm.2003.1236209","relation":{},"subject":[],"published":{"date-parts":[[2003]]}}}