Advisor: Deepak Garg
In this thesis, we study coeffect-based and effect-based refinement type systems for verification and complexity analysis of pure functional recursive programs. These type systems are relatively complete, which roughly means that they can be fine-tuned either for expressiveness or for tractability.
We consider two approaches: using coeffects and using effects. For the first approach, we generalise and simplify previous work by introducing a system that targets a call-by-push-value (CBPV) version of the programming language PCF, which supports higher-order recursive functions. We derive soundness and relative completeness for the new system. From this, these properties also follow for the old systems. In the effect-based approach, we also target CBPV.
For both approaches, we explain how the systems can be extended with features of modern programming language like polymorphism. One of the key properties of these systems is that they are compositional, which enables modular verification. We (informally) discuss efficient, sound and complete type inference algorithms that exploit this fact. Finally, we (informally) compare and combine both approaches, and we formalise a sound and relatively complete coeffect-based system from prior work in the proof assistant Coq.
| [1] | Samson Abramsky. Computational interpretations of linear logic. Theor. Comput. Sci., 111(1&2):3--57, 1993. [ DOI | http ] |
| [2] | Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Pierre-Yves Strub. A relational logic for higher-order programs. J. Funct. Program., 29:e16, 2019. [ DOI | http ] |
| [3] | Patrick Baillot, Gilles Barthe, and Ugo Dal Lago. Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. J. Autom. Reason., 63(4):813--855, 2019. [ DOI | http ] |
| [4] | Andrej Bauer and Matija Pretnar. An effect system for algebraic effects and handlers. Log. Methods Comput. Sci., 10(4), 2014. [ DOI | http ] |
| [5] | Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program extraction from normalization proofs. Stud Logica, 82(1):25--49, 2006. [ DOI | http ] |
| [6] | Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, and Christoph Weidenbach. A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason., 61(1-4):333--365, 2018. [ DOI | http ] |
| [7] | François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53--64, Wroclaw, Poland, August 2011. https://hal.inria.fr/hal-00790310. |
| [8] | Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Zhong Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 351--370. Springer, 2014. [ DOI | http ] |
| [9] | Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. Relational cost analysis. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 316--329. ACM, 2017. [ http ] |
| [10] | Loïc Colson and Daniel Fredholm. System T, Call-by-Value and the Minimum Problem. Theor. Comput. Sci., 206(1-2):301--315, 1998. [ DOI | http ] |
| [11] | Ugo Dal Lago and Marco Gaboardi. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science, 8, 04 2011. [ DOI ] |
| [12] | Ugo Dal Lago and Barbara Petit. Linear Dependent Types in a Call-by-Value Scenario (Long Version). Science of Computer Programming, 84, 07 2012. [ DOI ] |
| [13] | Ugo Dal Lago and Barbara Petit. The Geometry of Types (Long Version). 10 2012. [ http ] |
| [14] | Ewen Denney. Refinement types for specification. In David Gries and Willem P. de Roever, editors, Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98) 8-12 June 1998, Shelter Island, New York, USA, volume 125 of IFIP Conference Proceedings, pages 148--166. Chapman & Hall, 1998. |
| [15] | Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified programming of Turing machines in Coq. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 114--128. ACM, 2020. [ DOI | http ] |
| [16] | Timothy S. Freeman and Frank Pfenning. Refinement types for ML. In David S. Wise, editor, Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268--277. ACM, 1991. [ DOI | http ] |
| [17] | Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 476--489. ACM, 2016. [ DOI | http ] |
| [18] | Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1--102, 1987. [ DOI | http ] |
| [19] | Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1--66, 1992. [ DOI | http ] |
| [20] | C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580, 1969. [ DOI | http ] |
| [21] | Jan Hoffmann. Types with potential: polynomial resource bounds via automatic amortized analysis. PhD thesis, Ludwig Maximilians University Munich, 2011. [ http ] |
| [22] | Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. Static determination of quantitative resource usage for higher-order programs. In Manuel V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 223--236. ACM, 2010. [ DOI | http ] |
| [23] | Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20, 2018. [ DOI | http ] |
| [24] | G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. Recurrence extraction for functional programs through call-by-push-value. Proc. ACM Program. Lang., 4(POPL):15:1--15:31, 2020. [ DOI | http ] |
| [25] | Peter Lammich. Automatic data refinement. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 84--99, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. [ DOI ] |
| [26] | Daan Leijen. Type directed compilation of row-typed algebraic effects. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 486--499. ACM, 2017. [ http ] |
| [27] | Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation. Springer, 2004. |
| [28] | Glen Mével, Jacques-Henri Jourdan, and François Pottier. Time credits and time receipts in iris. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 3--29. Springer, 2019. [ DOI | http ] |
| [29] | Robin Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17(3):348--375, 1978. [ DOI | http ] |
| [30] | Robin Milner, Mads Tofte, and David Macqueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997. |
| [31] | Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of program analysis. Springer, 1999. [ DOI | http ] |
| [32] | Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: Unified static analysis of context-dependence. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 385--397. Springer, 2013. [ DOI | http ] |
| [33] | Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: A calculus of context-dependent computation. 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 123--135. ACM, 2014. [ DOI | http ] |
| [34] | Gordon D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223--255, 1977. [ DOI | http ] |
| [35] | Vineet Rajani, Marco Gaboardi, and Jan Hoffmann. A unifying type-theory for higher-order (amortized) cost analysis. Proc. ACM Program. Lang. (to appear). |
| [36] | Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions. 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019. |
| [37] | Robert Endre Tarjan. Amortized computational complexity. SIAM Journal on Algebraic Discrete Methods, 6(2):306--318, 1985. |
| [38] | The Coq Development Team. The Coq proof assistant, version 8.11.0, January 2020. [ DOI | http ] |
| [39] | Hongwei Xi. Dependent ML: An approach to practical programming with dependent types. J. Funct. Program., 17(2):215--286, 2007. [ DOI | http ] |