{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T15:46:02Z","timestamp":1774799162120,"version":"3.50.1"},"reference-count":156,"publisher":"Emerald","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,10,5]]},"abstract":"<jats:p>Refinement types enrich a language\u2019s type system with logical predicates that circumscribe the set of values described by the type. These refinement predicates provide software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code, and give the type checker a way to enforce those properties at compile time. In this article, we distill the ideas developed in the substantial literature on refinement types into a unified tutorial that explains the key ingredients of modern refinement type systems. In particular, we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system.<\/jats:p>","DOI":"10.1561\/2500000032","type":"journal-article","created":{"date-parts":[[2021,10,5]],"date-time":"2021-10-05T07:09:59Z","timestamp":1633417799000},"page":"159-317","source":"Crossref","is-referenced-by-count":21,"title":["Refinement Types: A Tutorial"],"prefix":"10.1561","volume":"6","author":[{"given":"Ranjit","family":"Jhala","sequence":"first","affiliation":[{"name":"University of California , ,","place":["San Diego, USA"]}]},{"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute , ,","place":["Madrid, Spain"]}]}],"member":"140","published-online":{"date-parts":[[2021,10,5]]},"reference":[{"key":"2026032911010751100_ref001","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-09099-3_2","article-title":"Computing with an SMT Solver","volume-title":"Tests and Proofs","author":"Amin","year":"2014"},{"key":"2026032911010751100_ref002","volume-title":"An Introduction to Mathematical Logic and Type Theory","author":"Andrews","year":"2002"},{"key":"2026032911010751100_ref003","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., P.M\u00fcller, F.Poli, and A. J.Summers. (2019). \u201cLeveraging Rust Types for Modular Specification and Verification\u201d. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). URL: https:\/\/doi.org\/10.1145\/3360573.","DOI":"10.1145\/3360573"},{"key":"2026032911010751100_ref004","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"2026032911010751100_ref005","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-662-49122-5_3","article-title":"Predicate Abstraction for Linked Data Structures","author":"Bakst","year":"2016"},{"key":"2026032911010751100_ref006","doi-asserted-by":"crossref","unstructured":"Barnett, M., M.F\u00e4hndrich, K. R. M.Leino, P.M\u00fcller, W.Schulte, and H.Venter. (2011). \u201cSpecification and Verification: The Spec# Experience\u201d. In: Communications of the ACM. uRL: https:\/\/doi.org\/10.1145\/1953122.1953145.","DOI":"10.1145\/1953122.1953145"},{"key":"2026032911010751100_ref007","article-title":"The SMT-LIB Standard: Version 2.0","volume-title":"SMT","author":"Barrett","year":"2010"},{"key":"2026032911010751100_ref008","doi-asserted-by":"crossref","DOI":"10.1017\/S0960129503004122","article-title":"Type-based termination of recursive definitions","volume-title":"MSCS","author":"Barthe","year":"2004"},{"key":"2026032911010751100_ref009","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19718-5_2","article-title":"Polymorphic Contracts","author":"Belo","year":"2011"},{"key":"2026032911010751100_ref010","doi-asserted-by":"crossref","DOI":"10.1145\/1890028.1890031","article-title":"Refinement types for secure implementations","volume-title":"ACM TOPLAS","author":"Bengtson","year":"2011"},{"key":"2026032911010751100_ref011","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"2026032911010751100_ref012","doi-asserted-by":"crossref","DOI":"10.1145\/1863543.1863560","article-title":"Semantic Subtyping with an SMT Solver","author":"Bierman","year":"2010"},{"key":"2026032911010751100_ref013","volume-title":"The Binah Web Framework","author":"Lehmann","year":"2020"},{"key":"2026032911010751100_ref014","doi-asserted-by":"crossref","DOI":"10.1093\/comjnl\/32.2.122","article-title":"Algebraic Identities for Program Calculation","volume-title":"The Computer Journal","author":"Bird","year":"1989"},{"key":"2026032911010751100_ref015","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday","author":"Bjorner","year":"2015"},{"key":"2026032911010751100_ref016","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99392","volume-title":"Abstract F-Bounded Polymorphism for Object-Oriented Programming","author":"Canning","year":"1989"},{"key":"2026032911010751100_ref017","first-page":"228","article-title":"User-Defined Data Types as an Aid to Verifying LISP Programs","author":"Cartwright","year":"1976"},{"key":"2026032911010751100_ref018","doi-asserted-by":"crossref","DOI":"10.1145\/2384616.2384659","article-title":"Dependent Types for JavaScript","volume-title":"OOPLSA","author":"Chugh","year":"2012"},{"key":"2026032911010751100_ref019","first-page":"53","article-title":"Simple Ownership Types for Object Containment","author":"Clarke","year":"2001"},{"key":"2026032911010751100_ref020","doi-asserted-by":"crossref","DOI":"10.4204\/EPTCS.149.8","article-title":"OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse","author":"Cok","year":"2014"},{"key":"2026032911010751100_ref021","volume-title":"Collatz Conjecture","year":"2021"},{"key":"2026032911010751100_ref022","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"2026032911010751100_ref023","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-12896-4_359","article-title":"Mathematics as Programming","author":"Constable","year":"1983"},{"key":"2026032911010751100_ref024","doi-asserted-by":"crossref","DOI":"10.1145\/1941487.1941509","article-title":"Proving program termination","volume-title":"Commun. ACM","author":"Cook","year":"2011"},{"key":"2026032911010751100_ref025","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-15983-5_13","article-title":"Constructions: A higher order proof system for mechanizing mathematics","author":"Coquand","year":"1985"},{"key":"2026032911010751100_ref026","doi-asserted-by":"crossref","unstructured":"Coquand, T. and G.Huet. (1988). \u201cThe Calculus of Constructions\u201d. In: Information and Computation. URL: https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3.","DOI":"10.1016\/0890-5401(88)90005-3"},{"issue":"ICFP","key":"2026032911010751100_ref027","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3110270","article-title":"Local refinement typing","volume":"1","author":"Cosman","year":"2017","journal-title":"PACMPL"},{"key":"2026032911010751100_ref028","doi-asserted-by":"crossref","DOI":"10.1145\/582153.582176","article-title":"Principal Type-Schemes for Functional Programs","volume-title":"POPL","author":"Damas","year":"1982"},{"key":"2026032911010751100_ref029","doi-asserted-by":"crossref","DOI":"10.1145\/582153.582176","article-title":"Principal Type-Schemes for Functional Programs","volume-title":"POPL","author":"Damas","year":"1982"},{"issue":"3","key":"2026032911010751100_ref030","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","article-title":"Simplify: a theorem prover for program checking","volume":"52","author":"Detlefs","year":"2005","journal-title":"J. ACM"},{"issue":"11","key":"2026032911010751100_ref031","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1145\/947783.948659","article-title":"The NYU Ada Translator and Interpreter","volume":"15","author":"Dewar","year":"1980","journal-title":"SIGPLAN Not"},{"key":"2026032911010751100_ref032","volume-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"2026032911010751100_ref033","volume-title":"A Unified System of Type Refinements","author":"Dunfield","year":"2007"},{"key":"2026032911010751100_ref034","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-54434-1_18","article-title":"Extensible Datasort Refinements","author":"Dunfield","year":"2017"},{"key":"2026032911010751100_ref035","volume-title":"Bidirectional Typing","author":"Dunfield","year":"2020"},{"key":"2026032911010751100_ref036","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1145\/2500365.2500582","article-title":"Complete and easy bidirectional typechecking for higher-rank polymorphism","author":"Dunfield","year":"2013"},{"key":"2026032911010751100_ref037","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-48167-2_6","article-title":"Proof of Imperative Programs in Type Theory","author":"Filli\u00e2tre","year":"1998"},{"key":"2026032911010751100_ref038","doi-asserted-by":"crossref","DOI":"10.1145\/1111037.1111059","article-title":"Hybrid Type Checking","volume-title":"POPL","author":"Flanagan","year":"2006"},{"key":"2026032911010751100_ref039","doi-asserted-by":"crossref","unstructured":"Flanagan, C. and K.Leino. (2001). \u201cHoudini, an Annotation Assistant for ESC\/Java\u201d. URL: citeseer.ist.psu.edu\/flanagan00houdini.html.","DOI":"10.1007\/3-540-45251-6_29"},{"key":"2026032911010751100_ref040","doi-asserted-by":"crossref","DOI":"10.1145\/155090.155113","article-title":"The Essence of Compiling with Continuations","volume-title":"PLDI","author":"Flanagan","year":"1993"},{"key":"2026032911010751100_ref041","doi-asserted-by":"crossref","unstructured":"Flanagan, C., K. R. M.Leino, M.Lillibridge, G.Nelson, J. B.Saxe, and R.Stata. (2002). \u201cExtended Static Checking for Java\u201d. In: Programming Language Design and Implementation (PLDI). URL: https:\/\/doi.org\/10.1145\/512529.512558.","DOI":"10.1145\/512557.512558"},{"key":"2026032911010751100_ref042","doi-asserted-by":"crossref","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd","year":"1967"},{"key":"2026032911010751100_ref043","doi-asserted-by":"crossref","DOI":"10.1145\/113445.113468","article-title":"Refinement Types for ML","volume-title":"PLDI","author":"Freeman","year":"1991"},{"key":"2026032911010751100_ref044","doi-asserted-by":"crossref","unstructured":"Freeman, T. and F.Pfenning. (1991b). \u201cRefinement Types for ML\u201d. In: Programming Language Design and Implementation (PLDI). URL: https:\/\/doi.org\/10.1145\/113445.113468.","DOI":"10.1145\/113445.113468"},{"key":"2026032911010751100_ref045","doi-asserted-by":"crossref","DOI":"10.1145\/1890028.1890030","article-title":"Automated termination proofs for Haskell by term rewriting","volume-title":"TPLS","author":"Giesl","year":"2011"},{"key":"2026032911010751100_ref046","first-page":"338","article-title":"A framework for numeric analysis of array operations","volume-title":"POPL","author":"Gopan","year":"2005"},{"key":"2026032911010751100_ref047","volume-title":"Logics and Languages for Reliability and Security","author":"Gordon","year":"2010"},{"issue":"3","key":"2026032911010751100_ref048","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/3064850","article-title":"Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types","volume":"39","author":"Gordon","year":"2017","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032911010751100_ref049","first-page":"72","volume-title":"CAV. LNCS 1254","author":"Graf","year":"1997"},{"key":"2026032911010751100_ref050","first-page":"93","article-title":"Sage: Hybrid checking for flexible specifications","author":"Gronski","year":"2006"},{"issue":"1-2","key":"2026032911010751100_ref051","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2500000010","article-title":"Program Synthesis","volume":"4","author":"Gulwani","year":"2017","journal-title":"Found. Trends Program. Lang"},{"key":"2026032911010751100_ref052","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/SYNASC49474.2019.00010","article-title":"The Science, Art, and Magic of Constrained Horn Clauses","author":"Gurfinkel","year":"2019"},{"key":"2026032911010751100_ref053","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/3314221.3314618","article-title":"Lazy counterfactual symbolic execution","author":"Hallahan","year":"2019"},{"issue":"OOPSLA","key":"2026032911010751100_ref054","doi-asserted-by":"publisher","first-page":"166:1","DOI":"10.1145\/3360592","article-title":"System FR: formalized foundations for the stainless verifier","volume":"3","author":"Hamza","year":"2019","journal-title":"Proc. ACM Program. Lang"},{"key":"2026032911010751100_ref055","doi-asserted-by":"crossref","unstructured":"Handley, M. A. T., N.Vazou, and G.Hutton. (2019). \u201cLiquidate Your Assets: Reasoning about Resource Usage in Liquid Haskell\u201d. In: Principles of Programming Languages (POPL). URL: https:\/\/doi.org\/10.1145\/3371092.","DOI":"10.1145\/3371092"},{"key":"2026032911010751100_ref056","doi-asserted-by":"crossref","DOI":"10.2307\/1995158","article-title":"The Principal Type-Scheme of an Object in Combinatory Logic","volume-title":"Transactions of the American Mathematical Society","author":"Hindley","year":"1969"},{"key":"2026032911010751100_ref057","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0059696","article-title":"Procedures and parameters: An axiomatic approach","volume-title":"Symposium on Semantics of Algorithmic Languages","author":"Hoare","year":"1971"},{"key":"2026032911010751100_ref058","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An Axiomatic Basis for Computer Programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Communications of the ACM"},{"key":"2026032911010751100_ref059","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","article-title":"Generalized Property Directed Reachability","author":"Hoder","year":"2012"},{"key":"2026032911010751100_ref060","doi-asserted-by":"publisher","first-page":"1","DOI":"10.23919\/FMCAD.2018.8603013","volume-title":"2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018","author":"Hojjat","year":"2018"},{"key":"2026032911010751100_ref061","article-title":"The formulae-as-types notion of construction","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"2026032911010751100_ref062","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/237721.240882","article-title":"Proving the Correctness of Reactive Systems Using Sized Types","author":"Hughes","year":"1996"},{"key":"2026032911010751100_ref063","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/360204.375719","article-title":"BI as an Assertion Language for Mutable Data Structures","volume-title":"POPL","author":"Ishtiaq","year":"2001"},{"key":"2026032911010751100_ref064","first-page":"298","volume-title":"TACAS 06. LNCS 2987","author":"Jhala","year":"2006"},{"key":"2026032911010751100_ref065","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-10575-8_15","volume-title":"Handbook of Model Checking","author":"Jhala","year":"2018"},{"key":"2026032911010751100_ref066","article-title":"Termination Analysis of the Untyped lamba-Calculus","volume-title":"RTA","author":"Jones","year":"2004"},{"key":"2026032911010751100_ref067","doi-asserted-by":"publisher","first-page":"e20","DOI":"10.1017\/S0956796818000151","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung","year":"2018","journal-title":"J. Funct. Program"},{"key":"2026032911010751100_ref068","article-title":"Refinement Types for Ruby","volume":"abs\/1711.09281","author":"Kazerounian","year":"2017","journal-title":"CoRR"},{"key":"2026032911010751100_ref069","doi-asserted-by":"crossref","DOI":"10.1145\/2908080.2908091","article-title":"Occurrence typing modulo theories","volume-title":"PLDI","author":"Kent","year":"2016"},{"key":"2026032911010751100_ref070","doi-asserted-by":"publisher","first-page":"396","DOI":"10.4230\/LIPIcs.ECOOP.2015.396","article-title":"Asynchronous Liquid Separation Types","author":"Kloos","year":"2015"},{"key":"2026032911010751100_ref071","doi-asserted-by":"crossref","DOI":"10.1145\/1481848.1481853","article-title":"Compositional and decidable checking for dependent contract types","volume-title":"PLPV","author":"Knowles","year":"2009"},{"key":"2026032911010751100_ref072","doi-asserted-by":"crossref","DOI":"10.1145\/1667048.1667051","article-title":"Hybrid type checking","volume-title":"TOPLAS","author":"Knowles","year":"2010"},{"key":"2026032911010751100_ref073","first-page":"157","article-title":"Dependent Types for Program Understanding","volume-title":"TACAS","author":"Komondoor","year":"2005"},{"issue":"3","key":"2026032911010751100_ref074","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","article-title":"SMT-based model checking for recursive programs","volume":"48","author":"Komuravelli","year":"2016","journal-title":"Formal Methods Syst. Des"},{"key":"2026032911010751100_ref075","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening","year":"2008"},{"key":"2026032911010751100_ref076","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"Computer Aided Verification","author":"Lahiri","year":"2009"},{"key":"2026032911010751100_ref077","first-page":"441","article-title":"STORM: Refinement Types for Secure Web Applications","author":"Lehmann","year":"2021"},{"key":"2026032911010751100_ref078","article-title":"An Extended Static Checker for Modula-3","volume-title":"Compiler Construction","author":"Leino","year":"1998"},{"key":"2026032911010751100_ref079","article-title":"Trigger selection strategies to stabilize program verifiers","volume-title":"CAV","author":"Leino","year":"2016"},{"key":"2026032911010751100_ref080","article-title":"Verified Calculations","volume-title":"VSTTE","author":"Leino","year":"2016"},{"key":"2026032911010751100_ref081","doi-asserted-by":"crossref","unstructured":"Leino, K. R. M.\n           (2010). \u201cDafny: An Automatic Program Verifier for Functional Correctness\u201d. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). URL: https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20.","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"2026032911010751100_ref082","doi-asserted-by":"crossref","unstructured":"Leino, R. and C.Pit-Claudel. (2016b). \u201cTrigger Selection Strategies to Stabilize Program Verifiers\u201d. In: Computer Aided Verification (CAV). URL: https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20.","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"2026032911010751100_ref083","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1145\/2429069.2429134","article-title":"Subjective Auxiliary State for Coarse-Grained Concurrency","author":"Ley-Wild","year":"2013"},{"issue":"2","key":"2026032911010751100_ref084","doi-asserted-by":"publisher","DOI":"10.1145\/3381915","article-title":"A Principled Approach to Selective Context Sensitivity for Pointer Analysis","volume":"42","author":"Li","year":"2020","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"2026032911010751100_ref085","doi-asserted-by":"crossref","unstructured":"Liu, Y., J.Parker, P.Redmond, L.Kuper, M.Hicks, and N.Vazou. (2020a). \u201cVerifying Replicated Data Types with Typeclass Refinements in Liquid Haskell\u201d. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). URL: https:\/\/doi.org\/10.1145\/3428284.","DOI":"10.1145\/3428284"},{"issue":"OOPSLA","key":"2026032911010751100_ref086","doi-asserted-by":"crossref","DOI":"10.1145\/3428284","article-title":"Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell","volume":"3","author":"Liu","year":"2020","journal-title":"Proc. ACM Program. Lang"},{"key":"2026032911010751100_ref087","doi-asserted-by":"crossref","unstructured":"Lovas, W. and F.Pfenning. (2010). \u201cRefinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance\u201d. In: Logical Methods in Computer Science. URL: http:\/\/dx.doi.org\/10.2168\/LMCS-6(4:5)2010.","DOI":"10.2168\/LMCS-6(4:5)2010"},{"key":"2026032911010751100_ref088","doi-asserted-by":"crossref","DOI":"10.1145\/3341708","article-title":"Dijkstra Monads for All","author":"Maillard","year":"2019"},{"key":"2026032911010751100_ref089","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-030-17184-1_2","article-title":"Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms","author":"Mart\u00ednez","year":"2019"},{"key":"2026032911010751100_ref090","article-title":"Towards a Mathematical Science of Computation","volume-title":"IFIP","author":"McCarthy","year":"1962"},{"key":"2026032911010751100_ref091","doi-asserted-by":"crossref","unstructured":"Melli\u00e8s, P.-A. and N.Zeilberger. (2015). \u201cFunctors Are Type Refinement Systems\u201d. In: Principles of Programming Languages (POPL). URL: https:\/\/doi.org\/10.1145\/2676726.2676970.","DOI":"10.1145\/2676726.2676970"},{"key":"2026032911010751100_ref092","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/1190216.1190247","article-title":"Logic-flow analysis of higher-order programs","volume-title":"POPL","author":"Might","year":"2007"},{"key":"2026032911010751100_ref093","doi-asserted-by":"crossref","unstructured":"Milner, R.\n           (1978). \u201cA theory of type polymorphism in programming\u201d. In: Journal of Computer and System Sciences. URL: https:\/\/doi.org\/10.1016\/0022-0000(78)90014-4.","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"2026032911010751100_ref094","doi-asserted-by":"crossref","DOI":"10.1017\/S0956796809007345","article-title":"Algebra of Programming in Agda: Dependent Types for Relational Program Derivation","volume-title":"J. Funct. Program","author":"Mu","year":"2009"},{"key":"2026032911010751100_ref095","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411204.1411237","article-title":"Ynot: dependent types for imperative programs","author":"Nanevski","year":"2008"},{"issue":"5-6","key":"2026032911010751100_ref096","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","article-title":"Hoare type theory, polymorphism and separation","volume":"18","author":"Nanevski","year":"2008","journal-title":"J. Funct. Program"},{"key":"2026032911010751100_ref097","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"POPL 97: Principles of Programming Languages","author":"Necula","year":"1997"},{"key":"2026032911010751100_ref098","volume-title":"Techniques for Program Verification","author":"Nelson","year":"1980"},{"key":"2026032911010751100_ref099","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1145\/3314221.3314643","article-title":"Size-Change Termination as a Contract: Dynamically and Statically Enforcing Termination for Higher-Order Programs","author":"Nguyen","year":"2019"},{"key":"2026032911010751100_ref100","article-title":"Types and Specifications","volume-title":"IFIP","author":"Nordstrom","year":"1983"},{"key":"2026032911010751100_ref101","doi-asserted-by":"crossref","DOI":"10.1007\/1-4020-8141-3_34","article-title":"Dynamic Typing with Dependent Types","volume-title":"IFIP TCS","author":"Ou","year":"2004"},{"key":"2026032911010751100_ref102","doi-asserted-by":"crossref","unstructured":"Parker, J., N.Vazou, and M.Hicks. (2019a). \u201cLWeb: Information Flow Security for Multi-Tier Web Applications\u201d. In: Principles of Programming Languages (POPL). URL: https:\/\/doi.org\/10.1145\/3290388.","DOI":"10.1145\/3290388"},{"issue":"POPL","key":"2026032911010751100_ref103","doi-asserted-by":"publisher","first-page":"75:1","DOI":"10.1145\/3290388","article-title":"LWeb: information flow security for multi-tier web applications","volume":"3","author":"Parker","year":"2019","journal-title":"Proc. ACM Program. Lang"},{"key":"2026032911010751100_ref104","doi-asserted-by":"crossref","unstructured":"Paulson, L. C., T.Nipkow, and M.Wenzel. (2019). \u201cFrom LCF to Isabelle\/HOL\u201d. In: Formal Aspects of Computing. URL: https:\/\/doi.org\/10.1007\/s00165-019-00492-1.","DOI":"10.1007\/s00165-019-00492-1"},{"key":"2026032911010751100_ref105","doi-asserted-by":"crossref","DOI":"10.1145\/1159803.1159811","article-title":"Simple unification-based type inference for GADTs","volume-title":"ICFP","author":"Peyton-Jones","year":"2006"},{"key":"2026032911010751100_ref106","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"2026032911010751100_ref107","doi-asserted-by":"crossref","DOI":"10.1145\/268946.268967","article-title":"Local Type Inference","volume-title":"POPL","author":"Pierce","year":"1998"},{"key":"2026032911010751100_ref108","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/LICS.2003.1210042","volume-title":"Logic in Computer Science","author":"Pierce","year":"2003"},{"key":"2026032911010751100_ref109","doi-asserted-by":"crossref","unstructured":"Plotkin, G.\n           (1977). \u201cLCF considered as a programming language\u201d. In: Theoretical Computer Science. URL: http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397577900445.","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"2026032911010751100_ref110","first-page":"32","article-title":"Transition Invariants","author":"Podelski","year":"2004"},{"key":"2026032911010751100_ref111","doi-asserted-by":"crossref","DOI":"10.1145\/2908080.2908093","article-title":"Program synthesis from polymorphic refinement types","volume-title":"PLDI","author":"Polikarpova","year":"2016"},{"issue":"ICFP","key":"2026032911010751100_ref112","doi-asserted-by":"publisher","first-page":"105:1","DOI":"10.1145\/3408987","article-title":"Liquid information flow control","volume":"4","author":"Polikarpova","year":"2020","journal-title":"Proc. ACM Program. Lang"},{"key":"2026032911010751100_ref113","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-36946-9_9","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"Potanin","year":"2013"},{"key":"2026032911010751100_ref114","doi-asserted-by":"crossref","unstructured":"Protzenko, J., B.Beurdouche, D.Merigoux, and K.Bhargavan. (2019). \u201cFormally Verified Cryptographic Web Applications in WebAssembly\u201d. In: Security and Privacy (SP). URL: http:\/\/dx.doi.org\/10.1109\/SP.2019.00064.","DOI":"10.1109\/SP.2019.00064"},{"key":"2026032911010751100_ref115","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/2491956.2462169","article-title":"Natural proofs for structure, data, and separation","author":"Qiu","year":"2013"},{"key":"2026032911010751100_ref116","first-page":"55","article-title":"Separation Logic: A Logic for Shared Mutable Data Structures","volume-title":"LICS","author":"Reynolds","year":"2002"},{"issue":"2","key":"2026032911010751100_ref117","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","article-title":"Classes of Recursively Enumerable Sets and Their Decision Problems","volume":"74","author":"Rice","year":"1953","journal-title":"Transactions of the American Mathematical Society"},{"key":"2026032911010751100_ref118","doi-asserted-by":"crossref","DOI":"10.1145\/1375581.1375602","article-title":"Liquid Types","volume-title":"PLDI","author":"Rondon","year":"2008"},{"key":"2026032911010751100_ref119","doi-asserted-by":"crossref","DOI":"10.1145\/1706299.1706316","article-title":"Low-Level Liquid Types","volume-title":"POPL","author":"Rondon","year":"2010"},{"key":"2026032911010751100_ref120","volume-title":"Constrained Horn Clause Solver Competition","author":"Ruemmer","year":"2021"},{"key":"2026032911010751100_ref121","volume-title":"Subtypes for Specifications: Predicate Subtyping in PVS","author":"Rushby","year":"1998"},{"issue":"3","key":"2026032911010751100_ref122","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1145\/514188.514190","article-title":"Parametric shape analysis via 3-valued logic","volume":"24","author":"Sagiv","year":"2002","journal-title":"ACM Trans. Program. Lang. Syst"},{"issue":"9","key":"2026032911010751100_ref123","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/1016848.1016878","article-title":"A Nanopass Infrastructure for Compiler Education","volume":"39","author":"Sarkar","year":"2004","journal-title":"SIGPLAN Not"},{"key":"2026032911010751100_ref124","doi-asserted-by":"crossref","DOI":"10.1145\/1596550.1596599","article-title":"Complete and decidable type inference for GADTs","volume-title":"ICFP","author":"Schrijvers","year":"2009"},{"key":"2026032911010751100_ref125","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1145\/2676726.2676996","article-title":"Manifest Contracts for Datatypes","author":"Sekiyama","year":"2015"},{"key":"2026032911010751100_ref126","doi-asserted-by":"crossref","DOI":"10.1007\/11575467_19","article-title":"Termination analysis of higher-order functional programs","volume-title":"APLAS","author":"Sereni","year":"2005"},{"key":"2026032911010751100_ref127","doi-asserted-by":"crossref","DOI":"10.1145\/53990.54007","article-title":"Control-Flow Analysis in Scheme","volume-title":"PLDI","author":"Shivers","year":"1988"},{"key":"2026032911010751100_ref128","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46425-5_24","article-title":"Alias Types","volume-title":"ESOP","author":"Smith","year":"2000"},{"key":"2026032911010751100_ref129","doi-asserted-by":"crossref","unstructured":"Sozeau, M., S.Boulier, Y.Forster, N.Tabareau, and T.Winterhalter. (2020). \u201cCoq Coq Correct. Verification of Type Checking and Erasure for Coq, in Coq\u201d. In: Principles of Programming Languages (POPL). URL: https:\/\/doi.org\/10.1145\/3371076.","DOI":"10.1145\/3371076"},{"key":"2026032911010751100_ref130","unstructured":"Sulzmann, M., M.Odersky, and M.Wehr. (1997). \u201cType Inference with Constrained Types\u201d. In: FOOL. URL: citeseer.ist.psu.edu\/article\/odersky99type.html."},{"key":"2026032911010751100_ref131","article-title":"Satisfiability Modulo Recursive Programs","volume-title":"SAS","author":"Suter","year":"2011"},{"key":"2026032911010751100_ref132","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1145\/2034773.2034811","article-title":"Secure distributed programming with value-dependent types","author":"Swamy","year":"2011"},{"key":"2026032911010751100_ref133","doi-asserted-by":"crossref","unstructured":"Swamy, N., C.Hri\u0163cu, C.Keller, A.Rastogi, A.Delignat-Lavaud, S.Forest, K.Bhargavan, C.Fournet, P.-Y.Strub, M.Kohlweiss, J.-K.Zinzindohoue, and S.Zanella-B\u00e9guelin. (2016). \u201cDependent Types and Multi-Monadic Effects in F*\u201d. In: Principles of Programming Languages (POPL). URL: https:\/\/doi.org\/10.1145\/2837614.2837655.","DOI":"10.1145\/2837614.2837655"},{"key":"2026032911010751100_ref134","unstructured":"Timany, A. and M.Sozeau. (2018). \u201cCumulative Inductive Types in Coq\u201d. In: Formal Structures for Computation and Deduction (FSCD). URL: https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2018.29."},{"key":"2026032911010751100_ref135","doi-asserted-by":"crossref","DOI":"10.1145\/1328438.1328486","article-title":"The design and implementation of typed scheme","volume-title":"POPL","author":"Tobin-Hochstadt","year":"2008"},{"key":"2026032911010751100_ref136","article-title":"On computable numbers, with an application to the Eintscheidungsproblem","volume-title":"LMS","author":"Turing","year":"1936"},{"key":"2026032911010751100_ref137","first-page":"70","article-title":"Checking a Large Routine","author":"Turing","year":"1949"},{"key":"2026032911010751100_ref138","volume-title":"Types vs. Floyd-Hoare","author":"Jhala","year":"2019"},{"key":"2026032911010751100_ref139","doi-asserted-by":"crossref","DOI":"10.1145\/2784731.2784745","article-title":"Bounded refinement types","volume-title":"ICFP","author":"Vazou","year":"2015"},{"key":"2026032911010751100_ref140","article-title":"A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq","volume-title":"Haskell","author":"Vazou","year":"2017"},{"key":"2026032911010751100_ref141","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-37036-6_13","article-title":"Abstract Refinement Types","volume-title":"ESOP","author":"Vazou","year":"2013"},{"key":"2026032911010751100_ref142","doi-asserted-by":"crossref","DOI":"10.1145\/2628136.2628161","article-title":"Refinement Types for Haskell","volume-title":"ICFP","author":"Vazou","year":"2014"},{"key":"2026032911010751100_ref143","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/2633357.2633366","article-title":"LiquidHaskell: Experience with Refinement Types in the Real World","author":"Vazou","year":"2014"},{"issue":"POPL","key":"2026032911010751100_ref144","doi-asserted-by":"publisher","first-page":"53:1","DOI":"10.1145\/3158141","article-title":"Refinement reflection: complete verification with SMT","volume":"2","author":"Vazou","year":"2018","journal-title":"Proc. ACM Program. Lang"},{"key":"2026032911010751100_ref145","doi-asserted-by":"crossref","DOI":"10.1145\/2908080.2908110","article-title":"Refinement types for TypeScript","volume-title":"PLDI","author":"Vekris","year":"2016"},{"key":"2026032911010751100_ref146","doi-asserted-by":"crossref","DOI":"10.1145\/2699407","article-title":"Propositions As Types","volume-title":"Communications of the ACM","author":"Wadler","year":"2015"},{"key":"2026032911010751100_ref147","doi-asserted-by":"crossref","unstructured":"Wadler, P.\n           (1989). \u201cTheorems for Free\u201d. In: Functional Programming Languages and Computer Architecture (FPCA). URL: https:\/\/doi.org\/10.1145\/99370.99404.","DOI":"10.1145\/99370.99404"},{"key":"2026032911010751100_ref148","article-title":"Alias Types for Recursive Data Structures","volume-title":"Types in Compilation (TIC)","author":"Walker","year":"2000"},{"key":"2026032911010751100_ref149","unstructured":"Wenzel, M.\n           (2016). \u201cThe Isabelle System Manual\u201d. URL: https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle2016-1\/doc\/system.pdf."},{"key":"2026032911010751100_ref150","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-04132-2_2","volume-title":"Practical Aspects of Declarative Languages (PADL)","author":"Winant","year":"2014"},{"key":"2026032911010751100_ref151","article-title":"Dependent Types for Program Termination Verification","volume-title":"LICS","author":"Xi","year":"2001"},{"key":"2026032911010751100_ref152","doi-asserted-by":"crossref","DOI":"10.1145\/277650.277732","article-title":"Eliminating Array Bound Checking Through Dependent Types","volume-title":"PLDI","author":"Xi","year":"1998"},{"key":"2026032911010751100_ref153","unstructured":"Zeilberger, N.\n           (2016). \u201cPrinciples of Refinement Types\u201d. In: Oregon Programming Languages Summer School (OPLSS). URL: https:\/\/www.cs.bham.ac.uk\/~zeilbern\/oplss16\/refinements-notes.pdf."},{"key":"2026032911010751100_ref154","doi-asserted-by":"crossref","DOI":"10.1016\/S0304-3975(97)00062-5","article-title":"Indexed Types","volume-title":"TCS","author":"Zenger","year":"1997"},{"key":"2026032911010751100_ref155","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1145\/3192366.3192416","article-title":"A Data-Driven CHC Solver","author":"Zhu","year":"2018"},{"key":"2026032911010751100_ref156","doi-asserted-by":"publisher","first-page":"1789","DOI":"10.1145\/3133956.3134043","article-title":"HACL*: A Verified Modern Cryptographic Library","author":"Zinzindohou\u00e9","year":"2017"}],"container-title":["Foundations and Trends\u00ae in Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/6\/3-4\/159\/11044473\/2500000032en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftpgl\/article-pdf\/6\/3-4\/159\/11044473\/2500000032en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,29]],"date-time":"2026-03-29T15:01:25Z","timestamp":1774796485000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftpgl\/article\/6\/3-4\/159\/1328330\/Refinement-Types-A-Tutorial"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,5]]},"references-count":156,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2021,10,5]]}},"URL":"https:\/\/doi.org\/10.1561\/2500000032","relation":{},"ISSN":["2325-1107","2325-1131"],"issn-type":[{"value":"2325-1107","type":"print"},{"value":"2325-1131","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,5]]}}}