More Web Proxy on the site http://driver.im/

research-article

Open access

System FR: formalized foundations for the stainless verifier

Authors:

Nicolas Voirol,

Viktor KunčakAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 166, Pages 1 - 30

https://doi.org/10.1145/3360592

Published: 10 October 2019 Publication History

Abstract

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.

Supplementary Material

Auxiliary Archive (oopsla19main-p229-p-aux.zip)

* Stainless benchmarks * Stainless sources for release 0.4.0 * Coq proofs

Download
46.34 MB

a166-hamza (a166-hamza.webm)

Presentation at OOPSLA '19

Download
75.01 MB

References

[1]

Andreas Abel. 2004. Termination checking with types. ITA 38, 4 (2004), 277–319.

[2]

Andreas Abel. 2007. Type-based termination: a polymorphic lambda-calculus with sized higher-order types. Ph.D. Dissertation. Ludwig Maximilians University Munich. http://d- nb.info/984765581

[3]

Andreas Abel. 2008. Semi-Continuous Sized Types and Termination. Logical Methods in Computer Science 4, 2 (2008).

[4]

Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. In Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010 (EPiC Series), Ekaterina Komendantskaya, Ana Bove, and Milad Niqui (Eds.), Vol. 5. EasyChair, 18–32.

[5]

Andreas Abel. 2012. Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types. In Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012. (EPTCS), Dale Miller and Zoltán Ésik (Eds.), Vol. 77. 1–11.

[6]

Andreas Abel and Brigitte Pientka. 2013. Wellfounded recursion with copatterns: a unified approach to termination and productivity. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 185–196.

Digital Library

[7]

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra monads for free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 515–529. http://dl.acm.org/citation.cfm?id=3009878

Digital Library

[8]

Amal J. Ahmed. 2006. Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings (Lecture Notes in Computer Science), Peter Sestoft (Ed.), Vol. 3924. Springer, 69–83.

Digital Library

[9]

Nada Amin. 2016. Dependent Object Types. Ph.D. Dissertation. EPFL.

[10]

Abhishek Anand and Vincent Rahli. 2014. Towards a Formally Verified Proof Assistant. In Interactive Theorem Proving, Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing, Cham, 27–44.

[11]

Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. 2004. The Spec# Programming System: An Overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers (Lecture Notes in Computer Science), Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, and Traian Muntean (Eds.), Vol. 3362. Springer, 49–69.

Digital Library

[12]

Bruno Barras. 2010. Sets in Coq, Coq in Sets. J. Formalized Reasoning 3, 1 (2010), 29–48.

[13]

Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, and Tarmo Uustalu. 2004. Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14, 1 (2004), 97–141.

Digital Library

[14]

Gilles Barthe, Benjamin Grégoire, and Colin Riba. 2008. A Tutorial on Type-Based Termination. In Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24 -March 1, 2008, Revised Tutorial Lectures. 100–152.

Digital Library

[15]

Yves Bertot and Pierre Castéran. 2004a. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer.

[16]

Yves Bertot and Pierre Castéran. 2004b. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Springer.

[17]

Régis Blanc and Viktor Kuncak. 2015. Sound reasoning about integral data types with a reusable SMT solver interface. In Proceedings of the 6th ACM SIGPLAN Symposium on Scala, Scala@PLDI 2015, Portland, OR, USA, June 15-17, 2015. 35–40.

Digital Library

[18]

Edwin Brady. 2013. Idris: general purpose programming with dependent types. In Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013, Matthew Might, David Van Horn, Andreas Abel, and Tim Sheard (Eds.). ACM, 1–2.

Digital Library

[19]

Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining proofs and programs in a dependently typed language. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 33–46.

Digital Library

[20]

Arthur Charguéraud. 2012. The Locally Nameless Representation. J. Autom. Reasoning 49, 3 (2012), 363–408.

[21]

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

[22]

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

[23]

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. 1998. Extended Static Checking. Technical Report 159. COMPAQ Systems Research Center.

[24]

Pietro Di Gianantonio and Marino Miculan. 2002. A Unifying Approach to Recursive and Co-recursive Definitions. In Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers (Lecture Notes in Computer Science), Herman Geuvers and Freek Wiedijk (Eds.), Vol. 2646. Springer, 148–161.

[25]

Jürgen Giesl, Matthias Raffelsieper, Peter Schneider-Kamp, Stephan Swiderski, and René Thiemann. 2011. Automated Termination Proofs for Haskell by Term Rewriting. ACM Trans. Program. Lang. Syst. 33, 2 (Feb. 2011), 7:1–7:39.

Digital Library

[26]

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–312.

[27]

Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke. 2004. Automated Termination Proofs with AProVE. In Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings. 210–220.

[28]

Jean-Yves Girard. 1971. Une Extension De L’Interpretation De Gödel a L’Analyse, Et Son Application a L’Elimination Des Coupures Dans L’Analyse Et La Theorie Des Types. Studies in Logic and the Foundations of Mathematics 63 (1971), 63–92.

[29]

Jean-Yves Girard. 1990. Proofs and types. Cambridge University Press. http://www.paultaylor.eu/stable/prot.pdf

Digital Library

[30]

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.

[31]

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. 2019. Lazy counterfactual symbolic execution. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019., Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 411–424.

Digital Library

[32]

Jad Hamza, Nicolas Voirol, and Viktor Kunčak. 2019. System FR as Foundations for Stainless. arXiv: cs.LO/1904.03482

[33]

Robert Harper. 2016. Practical foundations for programming languages. Cambridge University Press.

Digital Library

[34]

John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press.

Digital Library

[35]

John Harrison. 2017. HOL Light Tutorial. https://www.cl.cam.ac.uk/~jrh13/hol- light/tutorial.pdf . Retrieved 19 July 2019.

[36]

Lars Hupel and Viktor Kuncak. 2016. Translating Scala Programs to Isabelle/HOL (System Description). In International Joint Conference on Automated Reasoning (IJCAR).

Digital Library

[37]

Rohan Jacob-Rao, Brigitte Pientka, and David Thibodeau. 2018. Index-Stratified Types. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK (LIPIcs), Hélène Kirchner (Ed.), Vol. 108. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 19:1–19:17.

[38]

EPFL IC LARA. 2019. Stainles: Formal Verification for Scala. http://stainless.epfl.ch/ .

[39]

K Rustan M Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning. 348–370.

[40]

Rodolphe Lepigre. 2017. Semantics and Implementation of an Extension of ML for Proving Programs. (Sémantique et Implantation d’une Extension de ML pour la Preuve de Programmes). Ph.D. Dissertation. Grenoble Alpes University, France. https: //tel.archives- ouvertes.fr/tel- 01590363

[41]

Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In TLCA. 344–359.

[42]

Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. 2017. Higher order symbolic execution for contract verification and refutation. J. Funct. Program. 27 (2017), e3.

[43]

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002a. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer.

[44]

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002b. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol. 2283. Springer.

[45]

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden.

[46]

Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2018. Simplicitly: foundations and applications of implicit function types. PACMPL 2, POPL (2018), 42:1–42:29.

Digital Library

[47]

Martin Odersky, Lex Spoon, and Bill Venners. 2008. Programming in Scala: a comprehensive step-by-step guide. Artima Press.

[48]

Chris Okasaki. 1998. Purely Functional Data Structures. Cambridge University Press.

Digital Library

[49]

Aleksandar Prokopec and Martin Odersky. 2015. Conc-Trees for Functional and Parallel Programming. In Languages and Compilers for Parallel Computing, LCPC. 254–268.

Digital Library

[50]

Jorge Luis Sacchini. 2013. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. IEEE Computer Society, 233–242.

Digital Library

[51]

Georg Stefan Schmid and Viktor Kunčak. 2016. SMT-Based Checking of Predicate-Qualified Types for Scala. In Scala Symposium.

[52]

Matthieu Sozeau. 2010. Equations: A Dependent Pattern-Matching Compiler. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science), Matt Kaufmann and Lawrence C. Paulson (Eds.), Vol. 6172. Springer, 419–434.

Digital Library

[53]

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2019. The MetaCoq Project. (June 2019). https://hal.inria.fr/hal- 02167423 working paper or preprint.

[54]

Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak. 2011. Satisfiability Modulo Recursive Programs. In Static Analysis Symposium (SAS).

[55]

Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. ACM SIGPLAN Conference on Programming Language Design and Implementation (2013), 387.

Digital Library

[56]

W. W. Tait. 1967. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic 32, 2 (1967), 198–212.

[57]

Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In European Symposium on Programming, ESOP.

Digital Library

[58]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In International Conference on Functional Programming, ICFP. 269–282.

Digital Library

[59]

Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018. Refinement reflection: complete verification with SMT. PACMPL 2, POPL (2018), 53:1–53:31.

Digital Library

[60]

Nicolas Voirol. 2019. Verifying Functional Programs. Ph.D. Dissertation. EPFL.

[61]

Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak. 2015. Counter-example complete verification for higher-order functions. In Symposium on Scala, Scala 2015. 18–29.

Digital Library

[62]

Hongwei Xi. 2001. Dependent Types for Program Termination Verification. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. 231–242.

Cited By

Webbers Rvon Gleissenthall KJhala R(2024)Refinement Type RefutationsProceedings of the ACM on Programming Languages10.1145/36897458:OOPSLA2(962-987)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689745
Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Milovančević DFuhs CBucev MKunčak V(2024)Proving Termination via Measure Transfer in Equivalence CheckingIntegrated Formal Methods10.1007/978-3-031-76554-4_5(75-84)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_5
Show More Cited By

Index Terms

System FR: formalized foundations for the stainless verifier

Recommendations

System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...
Programming with binders and indexed data-types
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from ...
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 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
561
Total Downloads

Downloads (Last 12 months)129
Downloads (Last 6 weeks)15

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Webbers Rvon Gleissenthall KJhala R(2024)Refinement Type RefutationsProceedings of the ACM on Programming Languages10.1145/36897458:OOPSLA2(962-987)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689745
Borkowski MVazou NJhala R(2024)Mechanizing Refinement TypesProceedings of the ACM on Programming Languages10.1145/36329128:POPL(2099-2128)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632912
Milovančević DFuhs CBucev MKunčak V(2024)Proving Termination via Measure Transfer in Equivalence CheckingIntegrated Formal Methods10.1007/978-3-031-76554-4_5(75-84)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_5
Bordis TLeino K(2024)Free Facts: An Alternative to Inefficient Axioms in DafnyFormal Methods10.1007/978-3-031-71162-6_8(151-169)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_8
Chassot SKunčak V(2024)Verifying a Realistic Mutable Hash TableAutomated Reasoning10.1007/978-3-031-63498-7_18(304-314)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_18
Guo LKop C(2024)Higher-Order LCTRSs and Their TerminationProgramming Languages and Systems10.1007/978-3-031-57267-8_13(331-357)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_13
Vazou N(2023)On the Practicality and Soundness of Refinement TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.396.1396(1-3)Online publication date: 17-Nov-2023
https://doi.org/10.4204/EPTCS.396.1
Murali APeña LJhala RMadhusudan P(2023)Complete First-Order Reasoning for Properties of Functional ProgramsProceedings of the ACM on Programming Languages10.1145/36228357:OOPSLA2(1063-1092)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622835
Chiari MMandrioli DPontiggia FPradella M(2023)A Model Checker for Operator Precedence LanguagesACM Transactions on Programming Languages and Systems10.1145/360844345:3(1-66)Online publication date: 23-Sep-2023
https://dl.acm.org/doi/10.1145/3608443
Rehman BTomb A(2023)Correctness-by-Construction Meets Refinement TypesProceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3605156.3606449(8-10)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605156.3606449
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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