{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,25]],"date-time":"2025-07-25T10:26:19Z","timestamp":1753439179141,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>\n            This work introduces the novel concept of\n            <jats:italic>kind refinement<\/jats:italic>\n            , which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich\n            <jats:italic>kind<\/jats:italic>\n            specifications by means of predicates over\n            <jats:italic>types<\/jats:italic>\n            in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as tree-like data structures, with their kinds refined by logical constraints on such structures. Remarkably, the resulting typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type-directed meta-programming, which are often found in modern software development, but not typically expressible in a type-safe manner in general purpose languages. We validate our approach both formally and pragmatically by establishing the standard meta-theoretical results of type safety and via a prototype implementation of a kind checker, type checker and interpreter for our language.\n          <\/jats:p>","DOI":"10.1145\/3360557","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Refinement kinds: type-safe programming with practical type-level computation"],"prefix":"10.1145","volume":"3","author":[{"given":"Lu\u00eds","family":"Caires","sequence":"first","affiliation":[{"name":"Nova University of Lisbon, Portugal \/ NOVA-LINCS, Portugal"}]},{"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[{"name":"Nova University of Lisbon, Portugal \/ NOVA-LINCS, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103138"},{"key":"e_1_2_2_2_1","volume-title":"Germany (IFIP Conference Proceedings), Jeremy Gibbons and Johan Jeuring (Eds.)","volume":"243","author":"Altenkirch Thorsten","year":"2002","unstructured":"Thorsten Altenkirch and Conor McBride . 2002 . Generic Programming within Dependently Typed Programming. In Generic Programming, IFIP TC2\/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl , Germany (IFIP Conference Proceedings), Jeremy Gibbons and Johan Jeuring (Eds.) , Vol. 243 . Kluwer, 1\u201320. Thorsten Altenkirch and Conor McBride. 2002. Generic Programming within Dependently Typed Programming. In Generic Programming, IFIP TC2\/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl, Germany (IFIP Conference Proceedings), Jeremy Gibbons and Johan Jeuring (Eds.), Vol. 243. Kluwer, 1\u201320."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:12)2018"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"J. Bengtson K. Bhargavan C. Fournet A. D. Gordon and S. Maffeis. 2011. Refinement Types for Secure Implementations. ACM Trans. Program. Lang. Syst. (2011).  J. Bengtson K. Bhargavan C. Fournet A. D. Gordon and S. Maffeis. 2011. Refinement Types for Secure Implementations. ACM Trans. Program. Lang. Syst. (2011).","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_6_1","volume-title":"Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version). CoRR abs\/1908.00441","author":"Caires Lu\u00eds","year":"2019","unstructured":"Lu\u00eds Caires and Bernardo Toninho . 2019 . Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version). CoRR abs\/1908.00441 (2019). http:\/\/arxiv.org\/abs\/1908.00441 Lu\u00eds Caires and Bernardo Toninho. 2019. Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version). CoRR abs\/1908.00441 (2019). http:\/\/arxiv.org\/abs\/1908.00441"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004598"},{"key":"e_1_2_2_8_1","volume-title":"Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts","author":"Cardelli Luca","year":"1991","unstructured":"Luca Cardelli . 1991. Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts ( 1991 ), 431\u2013507. Luca Cardelli. 1991. Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts (1991), 431\u2013507."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806612"},{"key":"e_1_2_2_10_1","volume-title":"Smith","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable , Stuart F. Allen , Mark Bromley , Rance Cleaveland , J. F. Cremer , R. W. Harper , Douglas J. Howe , Todd B. Knoblock , N. P. Mendler , Prakash Panangaden , James T. Sasaki , and Scott F . Smith . 1986 . Implementing mathematics with the Nuprl proof development system. Prentice Hall . http:\/\/dl.acm.org\/citation.cfm?id=10510 Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice Hall. http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_2_2_11_1","unstructured":"CoqDevelopmentTeam. 2004. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.0.  CoqDevelopmentTeam. 2004. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.0."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173748"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_15_1","volume-title":"Jones","author":"Gaster Benedict R.","year":"1996","unstructured":"Benedict R. Gaster and Mark P . Jones . 1996 . A Polymorphic Type System for Extensible Records and Variants. Technical Report NOT TCS-TR-96-3. Functional Programming Research Group, Department of Computer Science, University of Nottingham . Benedict R. Gaster and Mark P. Jones. 1996. A Polymorphic Type System for Extensible Records and Variants. Technical Report NOT TCS-TR-96-3. Functional Programming Research Group, Department of Computer Science, University of Nottingham."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055070"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99603"},{"volume-title":"Extensional constructs in intensional type theory","author":"Hofmann Martin","key":"e_1_2_2_20_1","unstructured":"Martin Hofmann . 1997. Extensional constructs in intensional type theory . Springer . Martin Hofmann. 1997. Extensional constructs in intensional type theory. Springer."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375592"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314630"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017488"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/331960.331977"},{"key":"e_1_2_2_26_1","volume-title":"POPL","author":"Garrett Morris J.","year":"2019","unstructured":"J. Garrett Morris and James McKinna . 2019. Abstracting extensible data types: or, rows by any other name. PACMPL 3 , POPL ( 2019 ), 12:1\u201312:28. https:\/\/dl.acm.org\/citation.cfm?id=3290325 J. Garrett Morris and James McKinna. 2019. Abstracting extensible data types: or, rows by any other name. PACMPL 3, POPL (2019), 12:1\u201312:28. https:\/\/dl.acm.org\/citation.cfm?id=3290325"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908115"},{"key":"e_1_2_2_29_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages ( 1 st ed.). The MIT Press . Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.","edition":"1"},{"volume-title":"Advanced Topics in Types and Programming Languages","author":"Pierce Benjamin C.","key":"e_1_2_2_30_1","unstructured":"Benjamin C. Pierce . 2004. Advanced Topics in Types and Programming Languages . The MIT Press . Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_2_2_35_1","volume-title":"APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings. 485\u2013503","author":"Smaragdakis Yannis","year":"2015","unstructured":"Yannis Smaragdakis , George Balatsouras , George Kastrinis , and Martin Bravenboer . 2015 . More Sound Static Handling of Java Reflection. In Programming Languages and Systems - 13th Asian Symposium , APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings. 485\u2013503 . Yannis Smaragdakis, George Balatsouras, George Kastrinis, and Martin Bravenboer. 2015. More Sound Static Handling of Java Reflection. In Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings. 485\u2013503."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325724"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183281"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908110"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500599"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360557","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":44,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360557"],"URL":"https:\/\/doi.org\/10.1145\/3360557","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}