{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:03Z","timestamp":1790927523239,"version":"4.1.0"},"reference-count":56,"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-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"crossref","award":["200021_175676"],"award-info":[{"award-number":["200021_175676"]}],"id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"crossref"}]}],"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>We present the design, implementation, and foundation of a verifier for higher-order functional programs with generics and recursive data types. Our system supports proving safety and termination using preconditions, postconditions and assertions. It supports writing proof hints using assertions and recursive calls. To formalize the soundness of the system we introduce System FR, a calculus supporting System F polymorphism, dependent refinement types, and recursive types (including recursion through contravariant positions of function types). Through the use of sized types, System FR supports reasoning about termination of lazy data structures such as streams. We formalize a reducibility argument using the Coq proof assistant and prove the soundness of a type-checker with respect to call-by-value semantics, ensuring type safety and normalization for typeable programs. Our program verifier is implemented as an alternative verification-condition generator for the Stainless tool, which relies on the Inox SMT-based solver backend for automation. We demonstrate the efficiency of our approach by verifying a collection of higher-order functional programs comprising around 14000 lines of polymorphic higher-order Scala code, including graph search algorithms, basic number theory, monad laws, functional data structures, and assignments from popular Functional Programming MOOCs.<\/jats:p>","DOI":"10.1145\/3360592","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":33,"title":["System FR: formalized foundations for the stainless verifier"],"prefix":"10.1145","volume":"3","author":[{"given":"Jad","family":"Hamza","sequence":"first","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Voirol","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2004015"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:3)2008"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.29007\/322q"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1695"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_3"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774975.2774980"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428118"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_21_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_22_1","volume-title":"International Symposium on Artificial Intelligence and Mathematics, ISAIM 2016","author":"de Moura Leonardo","year":"2016","unstructured":"Leonardo de Moura . 2016 . Formalizing Mathematics using the Lean Theorem Prover . In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2016 , Fort Lauderdale, Florida, USA , January 4-6, 2016. http:\/\/isaim2016.cs.virginia. edu\/papers\/ISAIM2016_Proofs_DeMoura.pdf Leonardo de Moura. 2016. Formalizing Mathematics using the Lean Theorem Prover. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2016, Fort Lauderdale, Florida, USA, January 4-6, 2016. http:\/\/isaim2016.cs.virginia. edu\/papers\/ISAIM2016_Proofs_DeMoura.pdf"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890030"},{"key":"e_1_2_2_26_1","volume-title":"Rewriting techniques and Applications","author":"Giesl J","unstructured":"J Giesl , S Swiderski , P Schneider-Kamp , and R Thiemann . 2006. Automated termination analysis for Haskell: From term rewriting to programming languages . In Rewriting techniques and Applications , Vol. 4098 . 297\u2013312. J Giesl, S Swiderski, P Schneider-Kamp, and R Thiemann. 2006. Automated termination analysis for Haskell: From term rewriting to programming languages. In Rewriting techniques and Applications, Vol. 4098. 297\u2013312."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_15"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_2_2_29_1","volume-title":"Proofs and types","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard . 1990. Proofs and types . Cambridge University Press . http:\/\/www.paultaylor.eu\/stable\/prot.pdf Jean-Yves Girard. 1990. Proofs and types. Cambridge University Press. http:\/\/www.paultaylor.eu\/stable\/prot.pdf"},{"key":"e_1_2_2_30_1","unstructured":"M. J. C. Gordon and T. F. Melham. 1993. Introduction to HOL a theorem proving environment for higher-order logic. Cambridge University Press Cambridge England.  M. J. C. Gordon and T. F. Melham. 1993. Introduction to HOL a theorem proving environment for higher-order logic. Cambridge University Press Cambridge England."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"e_1_2_2_32_1","unstructured":"Jad Hamza Nicolas Voirol and Viktor Kun\u010dak. 2019. System FR as Foundations for Stainless. arXiv: cs.LO\/1904.03482  Jad Hamza Nicolas Voirol and Viktor Kun\u010dak. 2019. System FR as Foundations for Stainless. arXiv: cs.LO\/1904.03482"},{"key":"e_1_2_2_33_1","volume-title":"Practical foundations for programming languages","author":"Harper Robert","unstructured":"Robert Harper . 2016. Practical foundations for programming languages . Cambridge University Press . Robert Harper. 2016. Practical foundations for programming languages. Cambridge University Press."},{"key":"e_1_2_2_34_1","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison John","unstructured":"John Harrison . 2009. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press . John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press."},{"key":"e_1_2_2_35_1","volume-title":"HOL Light Tutorial. https:\/\/www.cl.cam.ac.uk\/~jrh13\/hol- light\/tutorial.pdf . Retrieved","author":"Harrison John","year":"2019","unstructured":"John Harrison . 2017. HOL Light Tutorial. https:\/\/www.cl.cam.ac.uk\/~jrh13\/hol- light\/tutorial.pdf . Retrieved 19 July 2019 . John Harrison. 2017. HOL Light Tutorial. https:\/\/www.cl.cam.ac.uk\/~jrh13\/hol- light\/tutorial.pdf . Retrieved 19 July 2019."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_38"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.19"},{"key":"e_1_2_2_38_1","volume-title":"Stainles: Formal Verification for Scala","author":"EPFL IC","year":"2019","unstructured":"EPFL IC LARA. 2019 . Stainles: Formal Verification for Scala . http:\/\/stainless.epfl.ch\/ . EPFL IC LARA. 2019. Stainles: Formal Verification for Scala. http:\/\/stainless.epfl.ch\/ ."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4{_}20"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000216"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158130"},{"key":"e_1_2_2_47_1","volume-title":"Programming in Scala: a comprehensive step-by-step guide","author":"Odersky Martin","unstructured":"Martin Odersky , Lex Spoon , and Bill Venners . 2008. Programming in Scala: a comprehensive step-by-step guide . Artima Press . Martin Odersky, Lex Spoon, and Bill Venners. 2008. Programming in Scala: a comprehensive step-by-step guide. Artima Press."},{"key":"e_1_2_2_48_1","volume-title":"Purely Functional Data Structures","author":"Okasaki Chris","unstructured":"Chris Okasaki . 1998. Purely Functional Data Structures . Cambridge University Press . Chris Okasaki. 1998. Purely Functional Data Structures. Cambridge University Press."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29778-1_16"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.29"},{"key":"e_1_2_2_51_1","volume-title":"SMT-Based Checking of Predicate-Qualified Types for Scala. In Scala Symposium.","author":"Schmid Georg Stefan","year":"2016","unstructured":"Georg Stefan Schmid and Viktor Kun\u010dak . 2016 . SMT-Based Checking of Predicate-Qualified Types for Scala. In Scala Symposium. Georg Stefan Schmid and Viktor Kun\u010dak. 2016. SMT-Based Checking of Predicate-Qualified Types for Scala. In Scala Symposium."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_2_2_53_1","volume-title":"The MetaCoq Project. (June","author":"Sozeau Matthieu","year":"2019","unstructured":"Matthieu Sozeau , Abhishek Anand , Simon Boulier , Cyril Cohen , Yannick Forster , Fabian Kunze , Gregory Malecha , Nicolas Tabareau , and Th\u00e9o Winterhalter . 2019. The MetaCoq Project. (June 2019 ). https:\/\/hal.inria.fr\/hal- 02167423 working paper or preprint. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Th\u00e9o Winterhalter. 2019. The MetaCoq Project. (June 2019). https:\/\/hal.inria.fr\/hal- 02167423 working paper or preprint."},{"key":"e_1_2_2_54_1","volume-title":"Satisfiability Modulo Recursive Programs. In Static Analysis Symposium (SAS).","author":"Suter Philippe","year":"2011","unstructured":"Philippe Suter , Ali Sinan K\u00f6ksal , and Viktor Kuncak . 2011 . Satisfiability Modulo Recursive Programs. In Static Analysis Symposium (SAS). Philippe Suter, Ali Sinan K\u00f6ksal, and Viktor Kuncak. 2011. Satisfiability Modulo Recursive Programs. In Static Analysis Symposium (SAS)."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774975.2774978"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932500"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360592","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":56,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360592"],"URL":"https:\/\/doi.org\/10.1145\/3360592","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}