Alejandro Aguirre
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.
We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.
Supplemental Material
Available for Download
zip
icfp17-main81-s.zip (793.8 KB)
Additional material for the paper, containing: * Summary of the semantics * Additional derivation rules * Paper proofs of the meta-theory * Paper proofs of soundness of the embeddings * Paper derivation of the examples * Additional examples
- Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. A Core Calculus of Dependency. In POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. 147–160. DOI: Google Scholar
Digital Library
- Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. 1993. Formal Parametric Polymorphism. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993. 157–170. DOI: Google ScholarDigital Library
- Peter Aczel and Nicola Gambino. 2000. Collection Principles in Dependent Type Theory. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers (Lecture Notes in Computer Science), Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.), Vol. 2277. Springer, 1–23. DOI: Google ScholarCross Ref
- Peter Aczel and Nicola Gambino. 2006. The generalised type-theoretic interpretation of constructive set theory. J. Symb. Log. 71, 1 (2006), 67–103. DOI: Google ScholarCross Ref
- Robin Adams and Zhaohui Luo. 2010. Classical predicative logic-enriched type theories. Ann. Pure Appl. Logic 161, 11 (2010), 1315–1345. DOI: Google ScholarCross Ref
- Bowen Alpern and Fred B. Schneider. 1985. Defining Liveness. Inf. Process. Lett. 21, 4 (1985), 181–185. DOI: Google ScholarCross Ref
- Kazuyuki Asada, Ryosuke Sato, and Naoki Kobayashi. 2016. Verifying relational properties of functional programs by first-order refinement. Science of Computer Programming (2016).Google Scholar
- Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational Verification Using Product Programs. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings. 200–214. DOI: Google ScholarCross Ref
- Gilles Barthe, Pedro R. D’Argenio, and Tamara Rezk. 2004. Secure Information Flow by Self-Composition. In 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28-30 June 2004, Pacific Grove, CA, USA. 100–114. DOI: Google ScholarCross Ref
- Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Béguelin. 2014. Probabilistic relational verification for cryptographic implementations. In Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14, Suresh Jagannathan and Peter Sewell (Eds.). 193–206. Google ScholarDigital Library
- Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 2015. Higher-order approximate relational refinement types for mechanism design and differential privacy. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). 55–68. Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. 90–101. DOI: Google ScholarDigital Library
- Gilles Barthe, Benjamin Grégoire, Justin Hsu, and Pierre-Yves Strub. 2017. Coupling proofs are probabilistic product programs. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 161–174. http://dl.acm.org/citation.cfm?id=3009896Google ScholarDigital Library
- Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin. 2012. Probabilistic relational reasoning for differential privacy. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. 97–110. DOI: Google ScholarDigital Library
- João Filipe Belo. 2007. Dependently Sorted Logic. In Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers (Lecture Notes in Computer Science), Marino Miculan, Ivan Scagnetto, and Furio Honsell (Eds.), Vol. 4941. Springer, 33–50. DOI: Google ScholarCross Ref
- Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations.. In Proceedings of the 31th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’04, Neil D. Jones and Xavier Leroy (Eds.). 14–25. Google ScholarDigital Library
- Lennart Beringer and Martin Hofmann. 2007. Secure information flow and program logics. In 20th IEEE Computer Security Foundations Symposium, CSF 2007, 6-8 July 2007, Venice, Italy. IEEE Computer Society, 233–248. DOI: Google ScholarDigital Library
- Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto. 2017. Deductive Verification with Relational Properties. In In Proc. of the 23th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Uppsala, Sweden. To Appear.Google Scholar
- Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational cost analysis. 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, 316–329. http://dl.acm.org/citation.cfm?id=3009858Google ScholarDigital Library
- Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In Proceedings of CSF’08. 51–65. Google ScholarDigital Library
- Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. Logical Methods in Computer Science 7, 2 (2011). DOI: Google ScholarCross Ref
- Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal. 2010. A relational modal logic for higher-order stateful ADTs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 185–198. DOI: Google ScholarDigital Library
- Joshua Dunfield and Frank Pfenning. 2004. Tridirectional typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones and Xavier Leroy (Eds.). ACM, 281–292. DOI: Google ScholarDigital Library
- Peter Dybjer. 1985. Program Verification in a Logical Theory of Constructions. In Functional Programming Languages and Computer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings (Lecture Notes in Computer Science), Jean-Pierre Jouannaud (Ed.), Vol. 201. Springer, 334–349. DOI: Google ScholarCross Ref
- Timothy S. Freeman and Frank Pfenning. 1991. Refinement Types for ML. In Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, David S. Wise (Ed.). ACM, 268–277. DOI: Google ScholarDigital Library
- Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear dependent types for differential privacy. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 357–370. DOI: Google ScholarDigital Library
- Neil Ghani, Fredrik Nordvall Forsberg, and Alex Simpson. 2016a. Comprehensive Parametric Polymorphism: Categorical Models and Type Theory. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 3–19. DOI: Google ScholarCross Ref
- Neil Ghani, Fredrik Nordvall Forsberg, and Alex Simpson. 2016b. Comprehensive Parametric Polymorphism: Categorical Models and Type Theory. In Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Lecture Notes in Computer Science), Bart Jacobs and Christof Löding (Eds.), Vol. 9634. Springer, 3–19. DOI: Google ScholarCross Ref
- John Hatcliff and Olivier Danvy. 1997. A computational formalization for partial evaluation. Mathematical Structures in Computer Science 7 (1997), 507–541. Google ScholarDigital Library
- Nevin Heintze and Jon G. Riecke. 1998. The SLam Calculus: Programming with Secrecy and Integrity. In POPL ’98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA, USA, January 19-21, 1998. 365–377. DOI: Google ScholarDigital Library
- B. Jacobs. 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam.Google Scholar
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 637–650. DOI: Google ScholarDigital Library
- Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. 2017. A relational model of types-and-effects in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 218–231. http://dl.acm.org/citation.cfm?id=3009877Google ScholarDigital Library
- Paul-André Melliès and Noam Zeilberger. 2015. Functors are Type Refinement Systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 3–16. DOI: Google ScholarDigital Library
- Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. 2013. Dependent Type Theory for Verification of Information Flow and Access Control Policies. ACM Trans. Program. Lang. Syst. 35, 2 (2013), 6:1–6:41. DOI: Google ScholarDigital Library
- Frank Pfenning. 2008. Church and Curry: Combining Intrinsic and Extrinsic Typing. In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, C.Benzmüller, C.Brown, J.Siekmann, and R.Statman (Eds.). College Publications, 303–338.Google Scholar
- Gordon Plotkin. 1973. Lambda-definability and logical relations. (1973).Google Scholar
- Gordon Plotkin. 1977. LCF considered as a programming language. Theoretical Computer Science 5, 3 (1977), 223 – 255. DOI: Google ScholarCross Ref
- Gordon D. Plotkin and Martín Abadi. 1993. A Logic for Parametric Polymorphism. In Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings. 361–375. DOI: Google ScholarCross Ref
- François Pottier and Vincent Simonet. 2002. Information flow inference for ML. In Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002. 319–330. DOI: Google ScholarDigital Library
- Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016. 57–69. DOI: Google ScholarDigital Library
- R. Statman. 1985. Logical relations and the typed λ-calculus. Information and Control 65, 2-3 (May 1985), 85–97. Google ScholarCross Ref
- Gordon Stewart, Anindya Banerjee, and Aleksandar Nanevski. 2013. Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. In 15th International Symposium on Principles and Practice of Declarative Programming, PPDP ’13, Madrid, Spain, September 16-18, 2013. 145–156. DOI: Google ScholarDigital Library
- 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. 2016. Dependent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256–270. DOI: Google ScholarDigital Library
- William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I. J. Symb. Log. 32, 2 (1967), 198–212. DOI: Google ScholarCross Ref
- Tachio Terauchi and Alex Aiken. 2005. Secure Information Flow as a Safety Problem. In Static Analysis Symposium, Chris Hankin and Igor Siveroni (Eds.), Vol. 3672. 352–367. Google ScholarDigital Library
- Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269–282. DOI: Google ScholarDigital Library
- Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. 1996. A sound type system for secure flow analysis. Journal of Computer Security 4, 3 (1996), 1–21. Google ScholarCross Ref
- Hongwei Xi and Frank Pfenning. 1999. Dependent Types in Practical Programming. In POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999, Andrew W. Appel and Alex Aiken (Eds.). ACM, 214–227. DOI: Google ScholarDigital Library
- Hongseok Yang. 2007. Relational separation logic. 375, 1-3 (2007), 308–334.Google Scholar
- Anna Zaks and Amir Pnueli. 2008. CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In Formal Methods (Lecture Notes in Computer Science), Jorge Cuéllar, T. S. E. Maibaum, and Kaisa Sere (Eds.), Vol. 5014. 35–51.Google Scholar
- Noam Zeilberger. 2016. Principles of Type Refinement. (2016). http://noamz.org/oplss16/refinements- notes.pdf Notes for OPLSS 2016 school.Google Scholar
Index Terms
- A relational logic for higher-order programs
Recommendations
Verifying relational properties of functional programs by first-order refinement
We give an automated verification method for relational properties.The target is a higher-order functional language.We can use general refinement types as specifications under a certain restriction.We reduce type checking for general refinement types to ...
Verifying Relational Properties of Functional Programs by First-Order Refinement
PEPM '15: Proceedings of the 2015 Workshop on Partial Evaluation and Program ManipulationMuch progress has been made recently on fully automated verification of higher-order functional programs, based on refinement types and higher-order model checking. Most of those verification techniques are, however, based on first-order refinement ...
Relatively complete refinement type system for verification of higher-order non-deterministic programs
This paper considers verification of non-deterministic higher-order functional programs. Our contribution is a novel type system in which the types are used to express and verify (conditional) safety, termination, non-safety, and non-termination ...
Comments