research-article

Open access

Mechanizing Refinement Types

Authors:

Michael H. Borkowski,

Ranjit JhalaAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue POPL

Article No.: 70, Pages 2099 - 2128

https://doi.org/10.1145/3632912

Published: 05 January 2024 Publication History

Abstract

Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal metatheoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF, a core refinement calculus that combines semantic subtyping and parametric polymorphism. We develop a metatheory for this calculus and prove soundness of the type system. Finally, we give two mechanizations of our metatheory. First, we introduce data propositions, a novel feature that enables encoding derivation trees for inductively defined judgments as refined data types, and use them to show that LiquidHaskell’s refinement types can be used for mechanization. Second, we mechanize our results in Coq, which comes with stronger soundness guarantees than LiquidHaskell, thereby laying the foundations for mechanizing the metatheory of LiquidHaskell.

References

[1]

V. Astrauskas, A. Bílý, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers. 2022. The Prusti Project: Formal Verification for Rust (invited). In NASA Formal Methods (14th International Symposium). Springer, 88–108. https://link.springer.com/chapter/10.1007/978-3-031-06773-0_5

[2]

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses: The PoplMark Challenge. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Joe Hurd and Thomas F. Melham (Eds.) (Lecture Notes in Computer Science, Vol. 3603). Springer, 50–65. https://doi.org/10.1007/11541868_4

[3]

Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008. Engineering formal metatheory. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, George C. Necula and Philip Wadler (Eds.). ACM, 3–15. https://doi.org/10.1145/1328438.1328443

[4]

João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. 2011. Polymorphic Contracts. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, Gilles Barthe (Ed.) (Lecture Notes in Computer Science, Vol. 6602). Springer, 18–37. https://doi.org/10.1007/978-3-642-19718-5_2

[5]

Michael H. Borkowski, Niki Vazou, and Ranjit Jhala. 2023. Artifact for "Mechanizing Refinement Types". https://doi.org/10.5281/zenodo.8425960

[6]

Michael H. Borkowski, Niki Vazou, and Ranjit Jhala. 2023. Artifact Virtual Machine for "Mechanizing Refinement Types". https://doi.org/10.5281/zenodo.8425176

[7]

Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’05). Association for Computing Machinery, New York, NY, USA. 198–208. isbn:1595930906 https://doi.org/10.1145/1069774.1069793

[8]

Zilin Chen. 2022. A Hoare Logic Style Refinement Types Formalisation. In Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2022). Association for Computing Machinery, New York, NY, USA. 1–14. isbn:9781450394390 https://doi.org/10.1145/3546196.3550162

[9]

Thierry Coquand and Christine Paulin. 1990. Inductively Defined Types. In COLOG-88, Per Martin-Löf and Grigori Mints (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 50–66. isbn:978-3-540-46963-6 https://doi.org/10.1007/3-540-52335-9_47

[10]

Benjamin Cosman and Ranjit Jhala. 2017. Local refinement typing. Proc. ACM Program. Lang., 1, ICFP (2017), 26:1–26:27. https://doi.org/10.1145/3110270

[11]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337–340. isbn:978-3-540-78800-3 https://doi.org/10.1007/978-3-540-78800-3_24

[12]

Cormac Flanagan. 2006. Hybrid Type Checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’06). Association for Computing Machinery, New York, NY, USA. 245–256. isbn:1595930272 https://doi.org/10.1145/1111037.1111059

[13]

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI ’93). Association for Computing Machinery, New York, NY, USA. 237–247. isbn:0897915984 https://doi.org/10.1145/155090.155113

[14]

Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. 2011. Modular Code-Based Cryptographic Verification. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS ’11). Association for Computing Machinery, New York, NY, USA. 341–350. isbn:9781450309486 https://doi.org/10.1145/2046707.2046746

[15]

Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. 2002. Semantic Subtyping. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, 137–146. https://doi.org/10.1109/LICS.2002.1029823

[16]

Jad Elkhaleq Ghalayini and Neel Krishnaswami. 2023. Explicit Refinement Types. Proc. ACM Program. Lang., 7, ICFP (2023), Article 195, aug, 28 pages. https://doi.org/10.1145/3607837

[17]

Andrew D. Gordon and C. Fournet. 2010. Principles and Applications of Refinement Types. In Logics and Languages for Reliability and Security. IOS Press. https://doi.org/10.3233/978-1-60750-100-8-73

[18]

Michael Greenberg. 2013. Manifest Contracts. Ph.D. Dissertation. University of Pennsylvania. https://repository.upenn.edu/edissertations/468/

[19]

Jad Hamza, Nicolas Voirol, and Viktor Kuncak. 2019. System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang., 3, OOPSLA (2019), 166:1–166:30. https://doi.org/10.1145/3360592

[20]

Ranjit Jhala and Niki Vazou. 2021. Refinement Types: A Tutorial. Found. Trends Program. Lang., 6, 3-4 (2021), 159–317. https://doi.org/10.1561/2500000032

[21]

Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt. 2016. Occurrence Typing modulo Theories. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 296–309. isbn:9781450342612 https://doi.org/10.1145/2908080.2908091

[22]

Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova. 2020. Liquid resource types. Proc. ACM Program. Lang., 4, ICFP (2020), 106:1–106:29. https://doi.org/10.1145/3408988

[23]

Kenneth Knowles and Cormac Flanagan. 2009. Compositional Reasoning and Decidable Checking for Dependent Contract Types. In Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification (PLPV ’09). Association for Computing Machinery, New York, NY, USA. 27–38. isbn:9781605583303 https://doi.org/10.1145/1481848.1481853

[24]

Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust. Proc. ACM Program. Lang., 7, PLDI (2023), Article 169, jun, 25 pages. https://doi.org/10.1145/3591283

[25]

Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. 2021. STORM: Refinement Types for Secure Web Applications. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 441–459. isbn:978-1-939133-22-9 https://www.usenix.org/conference/osdi21/presentation/lehmann

[26]

Nico Lehmann and Éric Tanter. 2016. Formalizing Simple Refinement Types in Coq. In 2nd International Workshop on Coq for Programming Languages (CoqPL’16). St. Petersburg, FL, USA.

[27]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). https://doi.org/10.1007/978-3-642-17511-4_20

[28]

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy. 2019. Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms. In European Symposium on Programming (ESOP). https://doi.org/10.1007/978-3-030-17184-1_2

[29]

George C. Necula. 1997. Proof-Carrying Code. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97). Association for Computing Machinery, New York, NY, USA. 106–119. isbn:0897918533 https://doi.org/10.1145/263699.263712

[30]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. https://link.springer.com/book/10.1007/3-540-45949-9

[31]

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers.

[32]

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In Exploring New Frontiers of Theoretical Informatics, Jean-Jacques Levy, Ernst W. Mayr, and John C. Mitchell (Eds.). Springer US, Boston, MA. 437–450. isbn:978-1-4020-8141-5 https://doi.org/10.1007/1-4020-8141-3_34

[33]

James Parker, Niki Vazou, and Michael Hicks. 2019. LWeb: information flow security for multi-tier web applications. Proc. ACM Program. Lang., 3, POPL (2019), 75:1–75:30. https://doi.org/10.1145/3290388

[34]

Brigitte Pientka. 2010. Beluga: Programming with Dependent Types, Contextual Data, and Contexts. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–12. isbn:978-3-642-12251-4 https://doi.org/10.1007/978-3-642-12251-4_1

[35]

Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press. https://www.cis.upenn.edu/~bcpierce/tapl/

[36]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. 2022. Programming Language Foundations (Software Foundations, Vol. 2). Electronic textbook. https://softwarefoundations.cis.upenn.edu/

[37]

Randy Pollack. 1993. Closure Under Alpha-Conversion. In Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, Henk Barendregt and Tobias Nipkow (Eds.) (Lecture Notes in Computer Science, Vol. 806). Springer, 313–332. https://doi.org/10.1007/3-540-58085-9_82

[38]

Patrick Redmond, Gan Shen, and Lindsey Kuper. 2021. Toward Hole-Driven Development with Liquid Haskell. CoRR, abs/2110.04461 (2021), arXiv:2110.04461. arxiv:2110.04461

[39]

Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). Association for Computing Machinery, New York, NY, USA. 159–169. isbn:9781595938602 https://doi.org/10.1145/1375581.1375602

[40]

Didier Rémy. 2021. Type systems for programming languages. Course notes. https://www.doc.ic.ac.uk/~svb/TSfPL/

[41]

Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. 2017. Polymorphic Manifest Contracts, Revised and Resolved. ACM Trans. Program. Lang. Syst., 39, 1 (2017), 3:1–3:36. https://doi.org/10.1145/2994594

[42]

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. Coq Coq Correct. Verification of Type Checking and Erasure for Coq, in Coq. In Principles of Programming Languages (POPL). https://doi.org/10.1145/3371076

[43]

Matthieu Sozeau and Cyprien Mangin. 2019. Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq. Proc. ACM Program. Lang., 3, ICFP (2019), Article 86, jul, 29 pages. https://doi.org/10.1145/3341690

[44]

Martin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007. System F with Type Equality Coercions. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI ’07). Association for Computing Machinery, New York, NY, USA. 53–66. isbn:159593393X https://doi.org/10.1145/1190315.1190324

[45]

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Principles of Programming Languages (POPL). https://doi.org/10.1145/2837614.2837655

[46]

Sam Tobin-Hochstadt and Matthias Felleisen. 2008. The Design and Implementation of Typed Scheme. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). Association for Computing Machinery, New York, NY, USA. 395–406. isbn:9781595936899 https://doi.org/10.1145/1328438.1328486

[47]

Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow. 2017. A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq. In Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell (Haskell 2017). Association for Computing Machinery, New York, NY, USA. 63–74. isbn:9781450351829 https://doi.org/10.1145/3122955.3122963

[48]

Niki Vazou, Eric L. Seidel, and Ranjit Jhala. 2014. LiquidHaskell: Experience with Refinement Types in the Real World. In Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell (Haskell ’14). Association for Computing Machinery, New York, NY, USA. 39–51. isbn:9781450330411 https://doi.org/10.1145/2633357.2633366

[49]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). Association for Computing Machinery, New York, NY, USA. 269–282. isbn:9781450328739 https://doi.org/10.1145/2628136.2628161

[50]

Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018. Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang., 2, POPL (2018), 53:1–53:31. https://doi.org/10.1145/3158141

[51]

Philip Wadler. 1989. Theorems for Free!. In Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA ’89). Association for Computing Machinery, New York, NY, USA. 347–359. isbn:0897913280 https://doi.org/10.1145/99370.99404

Cited By

van der Poll J(2024)The Role of 4IR-5IR Leadership-Management in the Adoption of Formal MethodsSystems10.3390/systems1208030612:8(306)Online publication date: 18-Aug-2024
https://doi.org/10.3390/systems12080306
Chen Jde Mendonça JAyele BBekele BJalili SSharma PWohlfeil NZhang YJeannin J(2024)Synchronous Programming with Refinement TypesProceedings of the ACM on Programming Languages10.1145/36746578:ICFP(938-972)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674657

Index Terms

Mechanizing Refinement Types
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification

Recommendations

Explicit Refinement Types

We present λ_ert, a type theory supporting refinement types with <em>explicit proofs</em>. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties ...
Gradual refinement types
POPL '17

Refinement types are an effective language-based verification technique. However, as any expressive typing discipline, its strength is its weakness, imposing sometimes undesired rigidity. Guided by abstract interpretation, we extend the gradual typing ...
Refinement types for Haskell
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification

We present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue POPL

January 2024

2820 pages

EISSN:2475-1421

DOI:10.1145/3554315

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 January 2024

Published in PACMPL Volume 8, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
681
Total Downloads

Downloads (Last 12 months)681
Downloads (Last 6 weeks)104

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

van der Poll J(2024)The Role of 4IR-5IR Leadership-Management in the Adoption of Formal MethodsSystems10.3390/systems1208030612:8(306)Online publication date: 18-Aug-2024
https://doi.org/10.3390/systems12080306
Chen Jde Mendonça JAyele BBekele BJalili SSharma PWohlfeil NZhang YJeannin J(2024)Synchronous Programming with Refinement TypesProceedings of the ACM on Programming Languages10.1145/36746578:ICFP(938-972)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674657

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents