Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-24T21:49:53.108Z Has data issue: false hasContentIssue false
  • English
  • Français

A relational logic for higher-order programs

Part of: ICFP2017 JFP Research Articles

Published online by Cambridge University Press:  21 October 2019

ALEJANDRO AGUIRRE Open the ORCID record for ALEJANDRO AGUIRRE [Opens in a new window] ,
GILLES BARTHE ,
MARCO GABOARDI ,
DEEPAK GARG  and
PIERRE-YVES STRUB
ALEJANDRO AGUIRRE
Affiliation:
Imdea Software Institute & Universidad Politécnica de Madrid, Campus Montegancedo s/n 28223 Pozuelo de Alarcon, Madrid, Spain (e-mail: [email protected])
GILLES BARTHE
Affiliation:
Imdea Software Institute & MPI-SP, Campus Montegancedo s/n 28223 Pozuelo de Alarcon, Madrid, Spain (e-mail: [email protected])
MARCO GABOARDI
Affiliation:
University at Buffalo, The State University of New York (SUNY), Computer Science and Engineering 338B Davis Hall, Buffalo, NY 14260-2500, USA (e-mail: [email protected])
DEEPAK GARG
Affiliation:
Max Planck Institute for Software Systems (MPI-SWS), Campus E1 5 Saarbruecken, 66123, Germany (e-mail: [email protected])
PIERRE-YVES STRUB
Affiliation:
École Polytechnique, Laboratoire d’informatique (LIX), Bâtiment Alan Turing, 1 rue Honoré d’Estienne d’Orves, CS35003 91120 Palaiseau Cedex, France (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 flavor 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, 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.

Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e16
Copyright
© Cambridge University Press 2019 

References

Abadi, M., Banerjee, A., Heintze, N. & Riecke, J. G. (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, pp. 147–160.CrossRefGoogle Scholar
Abadi, M., Cardelli, L. & Curien, P.-L. (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, pp. 157–170.CrossRefGoogle Scholar
Aczel, P. & Gambino, N. (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, Callaghan, P., Luo, Z., McKinna, J. & Pollack, R. (eds), Lecture Notes in Computer Science, vol. 2277. Springer, pp. 1–23.Google Scholar
Aczel, P. & Gambino, N. (2006) The generalised type-theoretic interpretation of constructive set theory. J. Symb. Log. 71(1), 67–103.Google Scholar
Adams, R. & Luo, Z. (2010) Classical predicative logic-enriched type theories. Ann. Pure Appl. Logic 161(11), 1315–1345.CrossRefGoogle Scholar
Aguirre, A., Barthe, G., Birkedal, L., Bizjak, A., Gaboardi, M. & Garg, D. (2018) Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings, Ahmed, A. (ed), Lecture Notes in Computer Science, vol. 10801. Springer, pp. 214–241.CrossRefGoogle Scholar
Aguirre, A., Barthe, G., Gaboardi, M., Garg, D. & Strub, P.-Y. (2017) A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1–21:29.CrossRefGoogle Scholar
Alpern, B. & Schneider, F. B. (1985) Defining liveness. Inf. Process. Lett. 21(4), 181–185.CrossRefGoogle Scholar
Asada, K., Sato, R. & Kobayashi, N. (2016) Verifying relational properties of functional programs by first-order refinement. Sci. Comput. Program. 137, 2–62.CrossRefGoogle Scholar
Barthe, G., Crespo, J. M. & Kunz, C. (2011) Relational verification using product programs. In FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20–24, 2011. Proceedings, pp. 200–214.CrossRefGoogle Scholar
Barthe, G., D’Argenio, P. R. & Rezk, T. (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, pp. 100–114.CrossRefGoogle Scholar
Barthe, G., Fournet, C., Grégoire, B., Strub, P.-Y., Swamy, N. & Béguelin, S. Z. (2014) Probabilistic relational verification for cryptographic implementations. In Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, Jagannathan, S. & Sewell, P. (eds), pp. 193–206.CrossRefGoogle Scholar
Barthe, G., Gaboardi, M., Gallego Arias, E. J., Hsu, J., Roth, A. & Strub, P.-Y. (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, Rajamani, S. K. & Walker, D. (eds), pp. 55–68.CrossRefGoogle Scholar
Barthe, G., Grégoire, B. & Béguelin, S. Z. (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, pp. 90–101.CrossRefGoogle Scholar
Barthe, G., Grégoire, B., Hsu, J. & Strub, P.-Y. (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, pp. 161–174.CrossRefGoogle Scholar
Barthe, G., Köpf, B., Olmedo, F. & Béguelin, S. Z. (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, pp. 97–110.CrossRefGoogle Scholar
Belo, J. F. (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, Miculan, M., Scagnetto, I. & Honsell, F. (eds), Lecture Notes in Computer Science, vol. 4941. Springer, pp. 33–50.Google Scholar
Benton, N. (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, Jones, N. D. & Leroy, X. (eds), pp. 14–25.CrossRefGoogle Scholar
Beringer, L. & Hofmann, M. (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, pp. 233–248.CrossRefGoogle Scholar
Blatter, L., Kosmatov, N., Gall, P. L. & Prevosto, V. (2017) Deductive verification with relational properties. In Proceedings of the 23th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Uppsala, Sweden, pp. 391–397. https://doi.org/10.1007/978-3-662-54577-5.CrossRefGoogle Scholar
Çiçek, E., Barthe, G., Gaboardi, M., Garg, D. & Hoffmann, J. (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, Castagna, G. & Gordon, A. D. (eds). ACM, pp. 316–329.CrossRefGoogle Scholar
Clarkson, M. R. & Schneider, F. B. (2008) Hyperproperties. In Proceedings of CSF ’08, pp. 51–65.CrossRefGoogle Scholar
Dreyer, D., Ahmed, A. & Birkedal, L. (2011) Logical step-indexed logical relations. Logical Methods Comput. Sci. 7(2).CrossRefGoogle Scholar
Dreyer, D., Neis, G., Rossberg, A. & Birkedal, L. (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, pp. 185–198.CrossRefGoogle Scholar
Dunfield, J. & Pfenning, F. (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, Jones, N. D. & Leroy, X. (eds). ACM, pp. 281–292.CrossRefGoogle Scholar
Dybjer, P. (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, Jouannaud, J.-P. (ed), Lecture Notes in Computer Science, vol. 201. Springer, pp. 334–349.CrossRefGoogle Scholar
Freeman, T. S. & Pfenning, F. (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, Wise, D. S. (ed). ACM, pp. 268–277.CrossRefGoogle Scholar
Gaboardi, M., Haeberlen, A., Hsu, J., Narayan, A. & Pierce, B. C. (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, Giacobazzi, R. & Cousot, R. (eds). ACM, pp. 357–370.CrossRefGoogle Scholar
Ghani, N., Forsberg, F. N. & Simpson, A. (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, pp. 3–19.Google Scholar
Ghani, N., Forsberg, F. N. & Simpson, A. (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, Jacobs, B. & Löding, C. (eds), Lecture Notes in Computer Science, vol. 9634. Springer, pp. 3–19.Google Scholar
Grimm, N., Maillard, K., Fournet, C., Hritcu, C., Maffei, M., Protzenko, J., Ramananandro, T., Rastogi, A., Swamy, N. & Béguelin, S. Z. (2018) A monadic framework for relational verification: Applied to information security, program equivalence, and optimizations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8–9, 2018, Andronick, J. & Felty, A. P. (eds). ACM, pp. 130–145.Google Scholar
Hatcliff, J. & Danvy, O. (1997) A computational formalization for partial evaluation. Math. Struct. Comput. Sci. 7, 507–541.CrossRefGoogle Scholar
Heintze, N. & Riecke, J. G. (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, pp. 365–377.CrossRefGoogle Scholar
Jacobs, B. (1999) Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Amsterdam: North Holland.Google Scholar
Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L. & Dreyer, D. (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, pp. 637–650.CrossRefGoogle Scholar
Kobayashi, N., Lozes, É. & Bruse, F. (2017) On the relationship between higher-order recursion schemes and higher-order fixpoint logic. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 246–259.CrossRefGoogle Scholar
Kobayashi, N., Tsukada, T. & Watanabe, K. (2018) Higher-order program verification via HFL model checking. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings, pp. 711–738.CrossRefGoogle Scholar
Krogh-Jespersen, M., Svendsen, K. & Birkedal, L. (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, pp. 218–231.CrossRefGoogle Scholar
Melliès, P.-A. & Zeilberger, N. (2015) Functors are type refinement systems. In Rajamani, S. K. & Walker, D. (eds), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015. ACM, pp. 3–16.CrossRefGoogle Scholar
Nanevski, A., Banerjee, A. & Garg, D. (2013) Dependent type theory for verification of information flow and access control policies. ACM Trans. Program. Lang. Syst. 35(2), 6:1–6:41.CrossRefGoogle Scholar
Pfenning, F. (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, Benzmüller, C., Brown, C., Siekmann, J. & Statman, R. (eds), Studies in Logic, vol. 17. College Publications, pp. 303–338.Google Scholar
Plotkin, G. (1973) Lambda-definability and logical relations. https://www.cl.cam.ac.uk/nk480/plotkin-logical-relations.pdf https://www.cl.cam.ac.uk/nk480/ https://www.cl.cam.ac.uk/ nk480/plotkin-logical-relations.pdfplotkin-logical-relations.pdfGoogle Scholar
Plotkin, G. (1977). LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255.CrossRefGoogle Scholar
Plotkin, G. D. & Abadi, M. (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, pp. 361–375.CrossRefGoogle Scholar
Pottier, F. & Simonet, V. (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, pp. 319–330.CrossRefGoogle Scholar
Radicek, I., Barthe, G., Gaboardi, M., Garg, D. & Zuleger, F. (2018) Monadic refinements for relational cost analysis. PACMPL 2(POPL), 36:1–36:32.Google Scholar
Sato, T., Aguirre, A., Barthe, G., Gaboardi, M., Garg, D. & Hsu, J. (2019) Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. PACMPL 3(POPL), 38:1–38:30.Google Scholar
Sousa, M. & Dillig, I. (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, pp. 57–69.CrossRefGoogle Scholar
Statman, R. (1985) Logical relations and the typed λ-calculus. Inf. Control 65(2–3), 85–97.CrossRefGoogle Scholar
Stewart, G., Banerjee, A. & Nanevski, A. (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, pp. 145–156.CrossRefGoogle Scholar
Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.-Y., Kohlweiss, M., Zinzindohoue, J. K. & Béguelin, S. Z. (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, Bodík, R. & Majumdar, R. (eds). ACM, pp. 256–270.CrossRefGoogle Scholar
Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2), 198–212.CrossRefGoogle Scholar
Terauchi, T. & Aiken, A. (2005) Secure information flow as a safety problem. In Static Analysis Symposium, Hankin, C. & Siveroni, I. (eds), LNCS, vol. 3672, pp. 352–367.CrossRefGoogle Scholar
The Coq Development Team (2018) The Coq proof assistant, version 8.8.0.Google Scholar
Unno, H., Torii, S. & Sakamoto, H. (2017) Automating induction for solving horn clauses. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part II, pp. 571–591.CrossRefGoogle Scholar
Vazou, N., Seidel, E. L., Jhala, R., Vytiniotis, D. & Jones, S. L. P. (2014). Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1–3, 2014, Jeuring, J. & Chakravarty, M. M. T. (eds). ACM, pp. 269–282.CrossRefGoogle Scholar
Volpano, D., Smith, G. & Irvine, C. (1996) A sound type system for secure flow analysis. J. Comput. Secur. 4(3), 1–21.Google Scholar
Wildmoser, M. & Nipkow, T. (2004) Certifying machine code safety: Shallow versus deep embedding. In Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14–17, 2004, Proceedings, pp. 305–320.CrossRefGoogle Scholar
Xi, H. & Pfenning, F. (1999) Dependent types in practical programming. In Appel, A. W. & Aiken, A. (eds), POPL ’99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20–22, 1999. ACM, pp. 214–227.CrossRefGoogle Scholar
Yang, H. (2007) Relational separation logic. Theor. Comput. Sci. 375(1–3), 308–334.CrossRefGoogle Scholar
Zaks, A. & Pnueli, A. (2008) CoVaC: Compiler validation by program analysis of the cross-product. In Formal Methods, Cuéllar, J., Maibaum, T. S. E. & Sere, Kaisa (eds), Lecture Notes in Computer Science, vol. 5014, pp. 35–51.CrossRefGoogle Scholar
Zeilberger, N. (2016) Principles of type refinement. Notes for OPLSS 2016 School.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.