{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:02Z","timestamp":1751660522350,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,2,28]],"date-time":"2019-02-28T00:00:00Z","timestamp":1551312000000},"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":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2019,3,31]]},"abstract":"<jats:p>We present a new, syntax-directed framework for Curry-style type systems with subtyping. It supports a rich set of features, and allows for a reasonably simple theory and implementation. The system we consider has sum and product types, universal and existential quantifiers, and inductive and coinductive types. The latter two may carry size invariants that can be used to establish the termination of recursive programs. For example, the termination of quicksort can be derived by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed polymorphism and (co-)induction. One of the key ideas is to separate the notion of size from recursion. We do not check the termination of programs directly, but rather show that their (circular) typing proofs are well-founded. Termination is then obtained using a standard (semantic) normalisation proof. To demonstrate the practicality of the system, we provide an implementation accepting all the examples discussed in the article.<\/jats:p>","DOI":"10.1145\/3285955","type":"journal-article","created":{"date-parts":[[2019,2,28]],"date-time":"2019-02-28T13:06:53Z","timestamp":1551359213000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Practical Subtyping for Curry-Style Languages"],"prefix":"10.1145","volume":"41","author":[{"given":"Rodolphe","family":"Lepigre","sequence":"first","affiliation":[{"name":"LAMA, CNRS, Univ. Savoie Mont Blanc and Inria, LSV, CNRS, Univ. Paris-Saclay"}]},{"given":"Christophe","family":"Raffalli","sequence":"additional","affiliation":[{"name":"LAMA, CNRS, Univ. Savoie Mont Blanc and IMERL, FING, UdelaR"}]}],"member":"320","published-online":{"date-parts":[[2019,2,28]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Types for the Scott Numerals. Retrieved on the","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi, Luca Cardelli, and Gordon Plotkin. 1993. Types for the Scott Numerals. Retrieved on the 12 September, 2016 from http:\/\/lucacardelli.name\/papers\/notes\/scott2.ps."},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/978-3-540-24727-2_3"},{"key":"e_1_2_1_3_1","volume-title":"Foetus - Termination Checker for Simple Functional Programs. Retrieved on the","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel. 1998. Foetus - Termination Checker for Simple Functional Programs. Retrieved on the 7 July, 2017 from http:\/\/www2.tcs.ifi.lmu.de\/&sim;abel\/foetus.pdf."},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/11874683_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/2500365.2500591"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/155183.155231"},{"key":"e_1_2_1_7_1","volume-title":"CSL (LIPIcs)","volume":"41","author":"Baelde David","year":"2015","unstructured":"David Baelde, Amina Doumane, and Alexis Saurin. 2015. Least and greatest fixed points in ludics. In CSL (LIPIcs), Vol. 41. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 549--566."},{"key":"e_1_2_1_8_1","volume-title":"CSL (LIPIcs)","volume":"62","author":"Baelde David","year":"2016","unstructured":"David Baelde, Amina Doumane, and Alexis Saurin. 2016. Infinitary proof theory: The multiplicative additive case. In CSL (LIPIcs), Vol. 62. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 42:1--42:17."},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1002\/malq.19930390137"},{"doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Blanqui. 2006. Decidability of type-checking in the calculus of algebraic constructions with size annotations. CoRR abs\/cs\/0608125.","key":"e_1_2_1_10_1","DOI":"10.1007\/11538363_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.5555\/1807662.1807678"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/11554554_8"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North-Holland, 479--504","author":"Cardelli Luca","year":"1990","unstructured":"Luca Cardelli and Xavier Leroy. 1990. Abstract types and the dot notation. In Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North-Holland, 479--504."},{"doi-asserted-by":"publisher","unstructured":"L. Cardelli S. Martini J. C. Mitchell and A. Scedrov. 1991. An extension of system F with subtyping. In Proceedings of TACS T. Ito and A. R. Meyer (Eds.) Lecture Notes in Computer Science Vol. 526. 750--770.","key":"e_1_2_1_14_1","DOI":"10.5555\/645867.670924"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1017\/S0956796806005867"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1145\/2603088.2603128"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/582153.582176"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1093\/logcom\/1.4.431"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/3009837.3009882"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_1_22_1","volume-title":"TACL (EPiC Series in Computing)","volume":"25","author":"Fortier J\u00e9r\u00f4me","year":"2013","unstructured":"J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for circular proofs. In TACL (EPiC Series in Computing), Vol. 25. EasyChair, 72--75."},{"key":"e_1_2_1_23_1","volume-title":"CSL (LIPIcs)","volume":"23","author":"Fortier J\u00e9r\u00f4me","year":"2013","unstructured":"J\u00e9r\u00f4me Fortier and Luigi Santocanale. 2013. Cuts for circular proofs: Semantics and cut-elimination. In CSL (LIPIcs), Vol. 23. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 248--262."},{"key":"e_1_2_1_24_1","volume-title":"ML Workshop.","author":"Garrigue Jacques","year":"1998","unstructured":"Jacques Garrigue. 1998. Programming with polymorphic variants. In ML Workshop."},{"doi-asserted-by":"publisher","unstructured":"Jean-Yves Girard Paul Taylor and Yves Lafont. 1989. Proofs and Types. Cambridge University Press.","key":"e_1_2_1_26_1","DOI":"10.5555\/64805"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.5555\/1928380.1928404"},{"key":"e_1_2_1_28_1","volume-title":"Grundlagen der Mathematik. Grundlehren der Mathematischen Wissenschaften","volume":"1","author":"Hilbert D.","unstructured":"D. Hilbert and P. Bernays. 1968. Grundlagen der Mathematik. Grundlehren der Mathematischen Wissenschaften, Vol. 1."},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_30_1","volume-title":"The size-change termination principle for constructor based languages. Logical Methods in Computer Science 10, 1","author":"Hyvernat Pierre","year":"2014","unstructured":"Pierre Hyvernat. 2014. The size-change termination principle for constructor based languages. Logical Methods in Computer Science 10, 1 (2014)."},{"doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Blanqui (INRIA). 2017. Size-Bases Termination of Higher-Order Rewrite Systems.","key":"e_1_2_1_31_1","DOI":"10.1017\/S0956796818000072"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1007\/11916277_8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.5555\/648064.747456"},{"key":"e_1_2_1_34_1","volume-title":"Un algorithme non typable dans le syst\u00e8me F. CRAS 304","author":"Krivine Jean-Louis","year":"1987","unstructured":"Jean-Louis Krivine. 1987. Un algorithme non typable dans le syst\u00e8me F. CRAS 304 (1987)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/944746.944709"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/360204.360210"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1007\/978-3-662-49498-1_19"},{"unstructured":"R. Lepigre and C. Raffalli. 2015. SubML Implementation. https:\/\/github.com\/rlepigre\/subml\/.","key":"e_1_2_1_39_1"},{"unstructured":"The Coq development team. 2004. The Coq Proof Assistant Reference Manual. LogiCal Project.","key":"e_1_2_1_40_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1016\/0890-5401(88)90009-0"},{"doi-asserted-by":"publisher","unstructured":"John C. Mitchell Sigurd Meldal and Neel Madhav. 1991. An extension of standard ML modules with subtyping and inheritance. In POPL. ACM 270--278. 10.1145\/99583.99620","key":"e_1_2_1_42_1","DOI":"10.1145\/99583.99620"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1145\/1481861.1481862"},{"unstructured":"Miche Parigot. 1992. Un r\u00e9curseur fortement normalisable et typable pour les entiers de Scott. Private communication.","key":"e_1_2_1_44_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1017\/S0956796806006034"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.5555\/509043"},{"unstructured":"C. Raffalli. 1998. Type checking in system F<sup>&eta;<\/sup>. In Pr\u00e9publication 98-05a du LAMA.","key":"e_1_2_1_48_1"},{"key":"e_1_2_1_49_1","volume-title":"The PhoX Proof Assistant. Retrieved on the","author":"Raffalli C.","year":"2016","unstructured":"C. Raffalli. 2008. The PhoX Proof Assistant. Retrieved on the 12 September, 2016 from https:\/\/www.lama.univ-smb.fr\/&sim;raffalli\/phox.html."},{"key":"e_1_2_1_50_1","volume-title":"The PML Programming Language. Retrieved","author":"Raffalli C.","year":"2016","unstructured":"C. Raffalli. 2012. The PML Programming Language. Retrieved 12 September, 2016 from https:\/\/www.lama.univ-smb.fr\/tracpml."},{"doi-asserted-by":"publisher","key":"e_1_2_1_51_1","DOI":"10.1145\/1086365.1086383"},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.1007\/978-3-662-44121-3_2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.5555\/647323.721503"},{"doi-asserted-by":"publisher","key":"e_1_2_1_54_1","DOI":"10.1109\/LICS.2013.29"},{"key":"e_1_2_1_55_1","volume-title":"Well-Founded Sized Types in the Calculus of (Co)Inductive Constructions. Retrieved on the","author":"Sacchini Jorge Luis","year":"2016","unstructured":"Jorge Luis Sacchini. 2015. Well-Founded Sized Types in the Calculus of (Co)Inductive Constructions. Retrieved on the 12 September, 2016 from http:\/\/cs.ioc.ee\/types15\/abstracts-book\/contrib30.pdf."},{"doi-asserted-by":"publisher","key":"e_1_2_1_56_1","DOI":"10.5555\/646794.704857"},{"doi-asserted-by":"publisher","key":"e_1_2_1_57_1","DOI":"10.1016\/S1571-0661(04)80370-0"},{"doi-asserted-by":"publisher","key":"e_1_2_1_58_1","DOI":"10.5555\/646794.704839"},{"key":"e_1_2_1_59_1","first-page":"365","article-title":"On global induction mechanisms in a &mu;-calculus with explicit approximations","volume":"37","author":"Sprenger Christoph","year":"2003","unstructured":"Christoph Sprenger and Mads Dam. 2003. On global induction mechanisms in a &mu;-calculus with explicit approximations. ITA 37, 4 (2003), 365--391. https:\/\/dblp.uni-trier.de\/rec\/bibtex\/journals\/ita\/SprengerD03.","journal-title":"ITA"},{"doi-asserted-by":"publisher","key":"e_1_2_1_60_1","DOI":"10.5555\/1754809.1754838"},{"doi-asserted-by":"publisher","key":"e_1_2_1_61_1","DOI":"10.1006\/inco.2001.2950"},{"volume-title":"Definite Descriptions and Choice Functions","author":"Heusinger Klaus Von","unstructured":"Klaus Von Heusinger. 1997. Definite Descriptions and Choice Functions. Springer Netherlands, Dordrecht, 61--91.","key":"e_1_2_1_62_1"},{"key":"e_1_2_1_63_1","volume-title":"LICS Proceedings. IEEE Computer Society, 176--185","author":"Wells J. B.","year":"1994","unstructured":"J. B. Wells. 1994. Typability and type-checking in the second-order lambda-calculus are equivalent and undecidable. In LICS Proceedings. IEEE Computer Society, 176--185."},{"doi-asserted-by":"publisher","key":"e_1_2_1_65_1","DOI":"10.1016\/S0168-0072(98)00047-5"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3285955","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3285955","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:44:14Z","timestamp":1750207454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3285955"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,28]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,3,31]]}},"alternative-id":["10.1145\/3285955"],"URL":"https:\/\/doi.org\/10.1145\/3285955","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2019,2,28]]},"assertion":[{"value":"2017-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-02-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}