{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T21:31:44Z","timestamp":1777498304147,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"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":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837655","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"256-270","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":221,"title":["Dependent types and multi-monadic effects in F*"],"prefix":"10.1145","author":[{"given":"Nikhil","family":"Swamy","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"Chantal","family":"Keller","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA \/ Inria, France"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Antoine","family":"Delignat-Lavaud","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS, France"}]},{"given":"Simon","family":"Forest","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS, France"}]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[{"name":"Inria, France"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA \/ Inria, France"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Markulf","family":"Kohlweiss","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Jean-Karim","family":"Zinzindohoue","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS, France"}]},{"given":"Santiago","family":"Zanella-B\u00e9guelin","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_1"},{"key":"e_1_3_2_1_4_1","volume-title":"13th International Workshop, CSL \u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999","author":"Altenkirch T.","year":"1999","unstructured":"T. Altenkirch and B. Reus . Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic , 13th International Workshop, CSL \u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999 , Proceedings , 1999 . T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, 13th International Workshop, CSL \u201999, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, 1999."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/774194.774197"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086375"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596565"},{"key":"e_1_3_2_1_16_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R. L.","year":"1986","unstructured":"R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , and S. F. Smith . Implementing Mathematics with the Nuprl Proof Development System . Prentice-Hall , 1986 . R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"e_1_3_2_1_17_1","first-page":"5246","article-title":"The Transport Layer Security (TLS) Protocol Version 1.2","author":"Dierks T.","year":"2008","unstructured":"T. Dierks and E. Rescorla . The Transport Layer Security (TLS) Protocol Version 1.2 . IETF RFC 5246 , 2008 . T. Dierks and E. Rescorla. The Transport Layer Security (TLS) Protocol Version 1.2. IETF RFC 5246, 2008.","journal-title":"IETF RFC"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_1_21_1","volume-title":"Cambridge University Press","author":"Harper R.","year":"2015","unstructured":"R. Harper . Practical foundations for programming languages. Cambridge University Press , second edition, 2015 . R. Harper. Practical foundations for programming languages. Cambridge University Press, second edition, 2015."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2201\/NiiPi.2013.10.3"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033954"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_26_1","volume-title":"LTA \u201908.","author":"Letouzey P.","year":"2008","unstructured":"P. Letouzey . Coq extraction, an overview . In LTA \u201908. 2008 . P. Letouzey. Coq extraction, an overview. In LTA \u201908. 2008."},{"key":"e_1_3_2_1_27_1","volume-title":"IFIP Congress","author":"McCarthy J.","year":"1962","unstructured":"J. McCarthy . Towards a mathematical science of computation . In IFIP Congress , 1962 . J. McCarthy. Towards a mathematical science of computation. In IFIP Congress, 1962."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/586110.586125"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_3_2_1_34_1","volume-title":"ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings.","author":"Sch\u00e4fer S.","year":"2015","unstructured":"S. Sch\u00e4fer , T. Tebbi , and G. Smolka . Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In Interactive Theorem Proving - 6th International Conference , ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. 2015 . S. Sch\u00e4fer, T. Tebbi, and G. Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. 2015."},{"key":"e_1_3_2_1_35_1","volume-title":"Subset Coercions in Coq","author":"Sozeau M.","year":"2007","unstructured":"M. Sozeau . Subset Coercions in Coq . In T. Altenkirch and C. McBride, editors, TYPES\u2019 06. 2007 . M. Sozeau. Subset Coercions in Coq. In T. Altenkirch and C. McBride, editors, TYPES\u201906. 2007."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_1_37_1","volume-title":"The Fourth Australasian Refinement Workshop","author":"Utting M.","year":"1996","unstructured":"M. Utting . Reasoning about aliasing . In The Fourth Australasian Refinement Workshop , 1996 . M. Utting. Reasoning about aliasing. In The Fourth Australasian Refinement Workshop, 1996."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500579"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837655","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837655","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:38Z","timestamp":1750211018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":36,"alternative-id":["10.1145\/2837614.2837655","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837655","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837655","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}