Document Open Access Logo

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types

Authors Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2021.18.pdf
  • Filesize: 1.01 MB
  • 29 pages

Document Identifiers

Author Details

Anish Tondwalkar
  • University of California, San Diego, CA, USA
Matthew Kolosick
  • University of California, San Diego, CA, USA
Ranjit Jhala
  • University of California, San Diego, CA, USA

Funding

This work was supported by NSF grant CCF-1911213.

Cite AsGet BibTex

Anish Tondwalkar, Matthew Kolosick, and Ranjit Jhala. Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ECOOP.2021.18

Abstract

Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express higher-order specifications. Ghost variables circumvent this limitation but are prohibitively tedious to use as the programmer must divine and explicate their values at all call-sites. We introduce Implicit Refinement Types which turn ghost variables into implicit pair and function types, in a way that lets the refinement typechecker automatically synthesize their values at compile time. Implicit Refinement Types further take advantage of refinement type information, allowing them to be used as a lightweight verification tool, rather than merely as a technique to automate programming tasks. We evaluate the utility of Implicit Refinement Types by showing how they enable the modular specification and automatic verification of various higher-order examples including stateful protocols, access control, and resource usage.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program constructs
  • Theory of computation → Program specifications
  • Theory of computation → Program verification
Keywords
  • Refinement Types
  • Implicit Parameters
  • Verification
  • Dependent Pairs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Retrieving paginated results - AWS SDK for java version 2, 2019. URL: https://docs.aws.amazon.com/sdk-for-java/v2/developer-guide/examples-pagination.html.
  2. Martín Abadi and Leslie Lamport. The existence of refinement mappings. In Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS 1988), Edinburgh, Scotland, UK, July 5-8, 1988, pages 165-175. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/LICS.1988.5115.
  3. Andrew W. Appel. Verified software toolchain. In Alwyn Goodloe and Suzette Person, editors, NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, volume 7226 of Lecture Notes in Computer Science, page 2. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28891-3_2.
  4. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations. In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008, pages 17-32. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/CSF.2008.27.
  5. Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified horn clauses. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 869-882. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_61.
  6. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. Horn clause solvers for program verification. In Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, and Wolfram Schulte, editors, Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, volume 9300 of Lecture Notes in Computer Science, pages 24-51. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23534-9_2.
  7. Edwin Brady. State machines all the way down. Draft, 2016. URL: https://www.idris-lang.org/drafts/sms.pdf.
  8. Edwin C. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming, 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  9. Adam Chlipala. The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA - September 25 - 27, 2013, pages 391-402. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500592.
  10. Benjamin Cosman and Ranjit Jhala. Local refinement typing. Proceedings of the ACM on Programming Languages, 1(ICFP):26:1-26:27, 2017. URL: https://doi.org/10.1145/3110270.
  11. Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects and implicits. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA, pages 341-360. ACM, 2010. URL: https://doi.org/10.1145/1869459.1869489.
  12. Bruno C. d. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi. The implicit calculus: a new foundation for generic programming. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China - June 11 - 16, 2012, pages 35-44. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254070.
  13. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  14. Dominique Devriese and Frank Piessens. On the bright side of type classes: instance arguments in agda. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 143-155. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034796.
  15. Jana Dunfield and Neelakantan R. Krishnaswami. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA - September 25 - 27, 2013, pages 429-442. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500582.
  16. Burak Emir, Andrew Kennedy, Claudio V. Russo, and Dachuan Yu. Variance and generalized constraints for c^# generics. In Dave Thomas, editor, ECOOP 2006 - Object-Oriented Programming, 20th European Conference, Nantes, France, July 3-7, 2006, Proceedings, volume 4067 of Lecture Notes in Computer Science, pages 279-303. Springer, 2006. URL: https://doi.org/10.1007/11785477_18.
  17. Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. Modular code-based cryptographic verification. In Yan Chen, George Danezis, and Vitaly Shmatikov, editors, Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 341-350. ACM, 2011. URL: https://doi.org/10.1145/2046707.2046746.
  18. Arjun Guha, Matthew Fredrikson, Benjamin Livshits, and Nikhil Swamy. Verified security for browser extensions. In 32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA, pages 115-130. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/SP.2011.36.
  19. Martin A. T. Handley, Niki Vazou, and Graham Hutton. Liquidate your assets: reasoning about resource usage in liquid haskell. Proceedings of the ACM on Programming Languages, 4(POPL):24:1-24:27, 2020. URL: https://doi.org/10.1145/3371092.
  20. Christian Heinlein. Implicit and dynamic parameters in C++. In David E. Lightfoot and Clemens A. Szyperski, editors, Modular Programming Languages, 7th Joint Modular Languages Conference, JMLC 2006, Oxford, UK, September 13-15, 2006, Proceedings, volume 4228 of Lecture Notes in Computer Science, pages 37-56. Springer, 2006. URL: https://doi.org/10.1007/11860990_4.
  21. Ranjit Jhala and Kenneth L. McMillan. A practical and complete approach to predicate refinement. In Holger Hermanns and Jens Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings, volume 3920 of Lecture Notes in Computer Science, pages 459-473. Springer, 2006. URL: https://doi.org/10.1007/11691372_33.
  22. Ming Kawaguchi, Patrick Maxim Rondon, and Ranjit Jhala. Type-based data structure verification. In Michael Hind and Amer Diwan, editors, Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009, pages 304-315. ACM, 2009. URL: https://doi.org/10.1145/1542476.1542510.
  23. Kenneth Knowles and Cormac Flanagan. Type reconstruction for general refinement types. In Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007, Proceedings, pages 505-519, 2007. URL: https://doi.org/10.1007/978-3-540-71316-6_34.
  24. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  25. Jeffrey R. Lewis, John Launchbury, Erik Meijer, and Mark Shields. Implicit parameters: Dynamic scoping with static types. In Mark N. Wegman and Thomas W. Reps, editors, POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, January 19-21, 2000, pages 108-118. ACM, 2000. URL: https://doi.org/10.1145/325694.325708.
  26. Tomer Libal. The unification algorithm, 2017. URL: https://github.com/FStarLang/FStar/wiki/The-unification-algorithm.
  27. Assia Mahboubi and Enrico Tassi. Canonical structures for the working coq user. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 19-34, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39634-2_5.
  28. Scott Moore, Christos Dimoulas, Dan King, and Stephen Chong. SHILL: A secure shell scripting language. In Jason Flinn and Hank Levy, editors, 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014, Broomfield, CO, USA, October 6-8, 2014, pages 183-199. USENIX Association, 2014. URL: https://doi.org/10.5555/2685048.268506.
  29. Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 229-240. ACM, 2008. URL: https://doi.org/10.1145/1411204.1411237.
  30. Ulf Norell. Dependently typed programming in agda. In Andrew Kennedy and Amal Ahmed, editors, Proceedings of TLDI 2009: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pages 1-2. ACM, 2009. URL: https://doi.org/10.1145/1481861.1481862.
  31. Susan S. Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319-340, 1976. URL: https://doi.org/10.1007/BF00268134.
  32. Benjamin C. Pierce and David N. Turner. Local type inference. ACM Transactions on Programming Language and Systems, 22(1):1-44, 2000. URL: https://doi.org/10.1145/345099.345100.
  33. Jon Postel. Transmission control protocol. STD 7, RFC Editor, September 1981. URL: http://www.rfc-editor.org/rfc/rfc793.txt.
  34. Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid types. In Rajiv Gupta and Saman P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 159-169. ACM, 2008. URL: https://doi.org/10.1145/1375581.1375602.
  35. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Verifying message-passing programs with dependent behavioural types. In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 502-516. ACM, 2019. URL: https://doi.org/10.1145/3314221.3322484.
  36. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, pages 266-278. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034811.
  37. Nikhil Swamy, Catalin Hritcu, 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. Dependent types and multi-monadic effects in F. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256-270. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837655.
  38. Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. Verifying higher-order programs with the dijkstra monad. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16-19, 2013, pages 387-398. ACM, 2013. URL: https://doi.org/10.1145/2491956.2491978.
  39. The Coq Development Team. The Coq Reference Manual, 2009. Google Scholar
  40. Anish Tondwalkar, Matthew Kolosick, and Ranjit Jhala. Refinements of futures past: Higher-order specification with implicit refinement types (extended version), 2021. URL: http://arxiv.org/abs/2105.01954.
  41. Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi. Automating relatively complete verification of higher-order functional programs. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy - January 23 - 25, 2013, pages 75-86. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429081.
  42. Niki Vazou, Alexander Bakst, and Ranjit Jhala. Bounded refinement types. In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 48-61. ACM, 2015. URL: https://doi.org/10.1145/2784731.2784745.
  43. Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. Abstract refinement types. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume 7792 of Lecture Notes in Computer Science, pages 209-228. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_13.
  44. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. Refinement types for haskell. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN International Conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 269-282. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628161.
  45. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement reflection: complete verification with SMT. Proceedings of the ACM on Programming Languages, 2(POPL):53:1-53:31, 2018. URL: https://doi.org/10.1145/3158141.
  46. Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 60-76. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75283.
  47. Leo White, Frédéric Bour, and Jeremy Yallop. Modular implicits. In Oleg Kiselyov and Jacques Garrigue, editors, Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014, volume 198 of EPTCS, pages 22-63, 2014. URL: https://doi.org/10.4204/EPTCS.198.2.
  48. Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Jack W. Davidson, Keith D. Cooper, and A. Michael Berman, editors, Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, 1998, pages 249-257. ACM, 1998. URL: https://doi.org/10.1145/277650.277732.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact