{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:29Z","timestamp":1772163989765,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,1,8]],"date-time":"2014-01-08T00:00:00Z","timestamp":1389139200000},"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":[[2014,1,8]]},"DOI":"10.1145\/2535838.2535883","type":"proceedings-article","created":{"date-parts":[[2014,1,14]],"date-time":"2014-01-14T08:40:06Z","timestamp":1389688806000},"page":"33-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":43,"title":["Combining proofs and programs in a dependently typed language"],"prefix":"10.1145","author":[{"given":"Chris","family":"Casinghino","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Vilhelm","family":"Sj\u00f6berg","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2014,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034807"},{"key":"e_1_3_2_2_3_1","volume-title":"Pitts","author":"Ahn K.Y.","year":"2012","unstructured":"Ahn , K.Y. , Sheard , T. , Fiore , M. , Pitts , A.M. : The Nax programming language (work in progress) ( 2012 ), talk presented at IFL 2012: the 24th Symposium on Implementation and Application of Functional Languages Ahn, K.Y., Sheard, T., Fiore, M., Pitts, A.M.: The Nax programming language (work in progress) (2012), talk presented at IFL 2012: the 24th Symposium on Implementation and Application of Functional Languages"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_2_7_1","first-page":"117","volume-title":"Handbook of Logic in Computer Science.","author":"Barendregt H.P.","year":"1992","unstructured":"Barendregt , H.P. : Lambda calculi with types . In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. pp. 117 -- 309 . Oxford University Press ( 1992 ) Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. pp. 117--309. Oxford University Press (1992)"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389461"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_3_2_2_12_1","first-page":"25","article-title":"Step-indexed normalization for a language with general recursion. In: MSFP '12","volume":"76","author":"Casinghino C.","year":"2012","unstructured":"Casinghino , C. , Sj\u00f6berg , V. , Weirich , S. : Step-indexed normalization for a language with general recursion. In: MSFP '12 : Mathematically Structured Functional Programming. EPTCS , vol. 76 , pp. 25 -- 39 ( 2012 ) Casinghino, C., Sj\u00f6berg, V., Weirich, S.: Step-indexed normalization for a language with general recursion. In: MSFP '12: Mathematically Structured Functional Programming. EPTCS, vol. 76, pp. 25--39 (2012)","journal-title":"Mathematically Structured Functional Programming. EPTCS"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_2_14_1","first-page":"183","volume-title":"Smith","author":"Constable R.L.","year":"1987","unstructured":"Constable , R.L. , Smith , S.F. : Partial objects in constructive type theory. In : Logic in Computer Science (LICS'87). pp. 183 -- 193 . IEEE ( 1987 ) Constable, R.L., Smith, S.F.: Partial objects in constructive type theory. In: Logic in Computer Science (LICS'87). pp. 183--193. IEEE (1987)"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646535.695848"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"key":"e_1_3_2_2_19_1","first-page":"219","volume-title":"ESOP'04: European Symposium on Programming. LNCS","volume":"2986","author":"Jia L.","year":"2004","unstructured":"Jia , L. , Walker , D. : Modal proofs as distributed programs (extended abstract) . In: ESOP'04: European Symposium on Programming. LNCS , vol. 2986 , pp. 219 -- 233 . Springer ( 2004 ) Jia, L., Walker, D.: Modal proofs as distributed programs (extended abstract). In: ESOP'04: European Symposium on Programming. LNCS, vol. 2986, pp. 219--233. Springer (2004)"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103780"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481851"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo Z.","year":"1994","unstructured":"Luo , Z. : Computation and Reasoning: A Type Theory for Computer Science . Oxford University Press , USA ( 1994 ) Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, USA (1994)"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754650"},{"key":"e_1_3_2_2_25_1","volume-title":"Harper","author":"Murphy VII, T.","year":"2007","unstructured":"Murphy , VII, T. , Crary , K. , Harper , R. : Type-safe distributed programming with ML 5. In : Trustworthy Global Computing 2007 (2007) Murphy, VII, T., Crary, K., Harper, R.: Type-safe distributed programming with ML5. In: Trustworthy Global Computing 2007 (2007)"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.009"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159811"},{"key":"e_1_3_2_2_30_1","volume-title":": Types and Programming Languages","author":"Pierce B.C.","year":"2002","unstructured":"Pierce , B.C. : Types and Programming Languages . MIT Press ( 2002 ) Pierce, B.C.: Types and Programming Languages. MIT Press (2002)"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268967"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88059-2_5"},{"key":"e_1_3_2_2_34_1","first-page":"112","article-title":"Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In: MSFP '12","volume":"76","author":"Sj\u00f6berg V.","year":"2012","unstructured":"Sj\u00f6berg , V. , Casinghino , C. , Ahn , K.Y. , Collins , N. , Eades III, H.D. , Fu , P. , Kimmell , G. , Sheard , T. , Stump , A. , Weirich , S. : Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In: MSFP '12 : Mathematically Structured Functional Programming. EPTCS , vol. 76 , pp. 112 -- 162 ( 2012 ) Sj\u00f6berg, V., Casinghino, C., Ahn, K.Y., Collins, N., Eades III, H.D., Fu, P., Kimmell, G., Sheard, T., Stump, A., Weirich, S.: Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In: MSFP '12: Mathematically Structured Functional Programming. EPTCS, vol. 76, pp. 112--162 (2012)","journal-title":"Mathematically Structured Functional Programming. EPTCS"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481856"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021953.2021972"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_2_40_1","volume-title":"Version 8.3. INRIA","author":"The Coq Development Team","year":"2010","unstructured":"The Coq Development Team : The Coq Proof Assistant Reference Manual , Version 8.3. INRIA ( 2010 ), http:\/\/coq.inria.fr\/V8.3\/refman\/ The Coq Development Team: The Coq Proof Assistant Reference Manual, Version 8.3. INRIA (2010), http:\/\/coq.inria.fr\/V8.3\/refman\/"},{"key":"e_1_3_2_2_41_1","volume-title":"Frequently Asked Questions. INRIA","author":"The Coq Development Team","year":"2011","unstructured":"The Coq Development Team : The Coq Proof Assistant , Frequently Asked Questions. INRIA ( 2011 ), http:\/\/coq.inria.fr\/faq\/ The Coq Development Team: The Coq Proof Assistant, Frequently Asked Questions. INRIA (2011), http:\/\/coq.inria.fr\/faq\/"},{"key":"e_1_3_2_2_42_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013","unstructured":"The Univalent Foundations Program : Homotopy Type Theory: Univalent Foundations of Mathematics ( 2013 ), http:\/\/arxiv.org\/abs\/1308.0729 The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics (2013), http:\/\/arxiv.org\/abs\/1308.0729"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantics of programming languages: an introduction","author":"Winskel G.","year":"1993","unstructured":"Winskel , G. : The formal semantics of programming languages: an introduction . MIT Press , Cambridge, MA, USA ( 1993 ) Winskel, G.: The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA (1993)"}],"event":{"name":"POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"San Diego California USA","acronym":"POPL '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535883","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2535838.2535883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:06Z","timestamp":1750219806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2535838.2535883"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1,8]]},"references-count":39,"alternative-id":["10.1145\/2535838.2535883","10.1145\/2535838"],"URL":"https:\/\/doi.org\/10.1145\/2535838.2535883","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2578855.2535883","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,1,8]]},"assertion":[{"value":"2014-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}