{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T08:56:34Z","timestamp":1781859394046,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"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":[[2015,1,14]]},"DOI":"10.1145\/2676726.2676970","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Functors are Type Refinement Systems"],"prefix":"10.1145","author":[{"given":"Paul-Andr\u00e9","family":"Melli\u00e8s","sequence":"first","affiliation":[{"name":"CNRS, Universit\u00e9 Paris Diderot, Sorbonne Paris Cit\u00e9, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Noam","family":"Zeilberger","sequence":"additional","affiliation":[{"name":"MSR-Inria Joint Centre, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","first-page":"2","volume":"8","author":"Atkey Robert","year":"2012","unstructured":"Robert Atkey, Patricia Johann, and Neil Ghani. Refining Inductive Types. LMCS, 8:2, 2012.","journal-title":"Refining Inductive Types. LMCS"},{"key":"e_1_3_2_2_2_1","volume-title":"Distributors at work.Notes from a course at TU Darmstadt","author":"B\u00e9nabou Jean","year":"2000","unstructured":"Jean B\u00e9nabou. Distributors at work.Notes from a course at TU Darmstadt in June 2000, taken by Thomas Streicher."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Lars Birkedal Noah Torp-Smith and Hongseok Yang.Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like languages. LMCS 5:2 2006.","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591370.2591396"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.3115\/1073012.1073045"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Claudio Hermida. Fibrations Logical predicates and indeterminates PhD thesis University of Edinburgh November 1993.","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_2_13_1","volume-title":"North Holland","author":"Jacobs Bart","year":"1999","unstructured":"Bart Jacobs. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, 1999."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2027223.2027240"},{"key":"e_1_3_2_2_15_1","volume-title":"CUP","author":"Kelly Max","year":"1982","unstructured":"Max Kelly. Basic concepts in enriched category theory. CUP, 1982."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1958.11989160"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/7517"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/2231513"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"e_1_3_2_2_22_1","unstructured":"Conor McBride. Ornamental Algebras Algebraic Ornaments. JFP (to appear). 9\/8\/2010 version available on author's website."},{"key":"e_1_3_2_2_23_1","first-page":"2","volume":"5","author":"O'Hearn Peter W.","year":"1999","unstructured":"Peter W. O'Hearn and David J. Pym. The Logic of Bunched Implications. BSL 5:2, 1999.","journal-title":"Pym. The Logic of Bunched Implications. BSL"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/646794.704850"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/910747"},{"key":"e_1_3_2_2_26_1","volume-title":"Pfenning. Refinement Types for Logical Frameworks. Workshop on Types for Proofs and Programs","author":"Frank","year":"1993","unstructured":"Frank Pfenning. Refinement Types for Logical Frameworks. Workshop on Types for Proofs and Programs, May 1993."},{"key":"e_1_3_2_2_27_1","first-page":"303","article-title":"Combining Intrinsic and Extrinsic Typing.","volume":"17","author":"Pfenning Frank","year":"2008","unstructured":"Frank Pfenning. Church and Curry: Combining Intrinsic and Extrinsic Typing.Studies in Logic 17, 2008, 303--338.","journal-title":"Studies in Logic"},{"key":"e_1_3_2_2_28_1","first-page":"372","article-title":"The Essence of Algol","volume":"345","author":"Reynolds John C.","year":"1981","unstructured":"John C. Reynolds. The Essence of Algol. Algorithmic Languages, 1981, 345--372.","journal-title":"Algorithmic Languages"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670915"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/307999"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. The Meaning of Types: from Intrinsic to Extrinsic Semantics. BRICS Report RS-00--32 Aarhus University December 2000.","DOI":"10.7146\/brics.v7i32.20167"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2676970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T08:34:18Z","timestamp":1781858058000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":32,"alternative-id":["10.1145\/2676726.2676970","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2676970","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2676970","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}