Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-22T00:20:13.037Z Has data issue: false hasContentIssue false
  • English
  • Français

A case study in programming coinductive proofs: Howe’s method

Published online by Cambridge University Press:  31 October 2018

ALBERTO MOMIGLIANO Open the ORCID record for ALBERTO MOMIGLIANO [Opens in a new window] ,
BRIGITTE PIENTKA  and
DAVID THIBODEAU
ALBERTO MOMIGLIANO
Affiliation:
Dipartimento di Informatica, Università degli Studi di Milano, Milano, Italy Email: alberto.momigliano@unimi.it
BRIGITTE PIENTKA
Affiliation:
School of Computer Science, McGill University, Montreal, Canada Email: bpientka@cs.mcgill.ca, david.thibodeau@mail.mcgill.ca
DAVID THIBODEAU
Affiliation:
School of Computer Science, McGill University, Montreal, Canada Email: bpientka@cs.mcgill.ca, david.thibodeau@mail.mcgill.ca
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.

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe’s method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga’s support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga’s reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga’s strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Special Issue 8: A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday , September 2019 , pp. 1309 - 1343
Copyright
© Cambridge University Press 2018 

References

Abel, A. (2012). Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In: Proceedings of the Invited Talk at 8th Workshop on Fixed-points in Computer Science (FICS’12) 1–11.Google Scholar
Abel, A. and Pientka, B. (2013). Well-founded recursion with copatterns: A unified approach to termination and productivity. In: Proceedings of the 18th International Conference on Functional Programming (ICFP’13) 185–196.Google Scholar
Abel, A. and Pientka, B. (2016). Well-founded recursion with copatterns and sized types. Journal of Functional Programming 26 e2.CrossRefGoogle Scholar
Abel, A., Pientka, B., Thibodeau, D. and Setzer, A. (2013). Copatterns: Programming infinite structures by observations. In: Proceedings of the 40th Symposium on Principles of Programming Languages (POPL’13), ACM Press, 27–38.CrossRefGoogle Scholar
Abramsky, S. (1991). A domain equation for bisimulation. Information and Computation 92 (2) 161–218.CrossRefGoogle Scholar
Ahmed, A. (2006). Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (eds.) Proceedings of the 15th European Symposium on Programming (ESOP’06), Springer, 69–83.Google Scholar
Allais, G., Chapman, J., McBride, C. and McKinna, J. (2017). Type-and-scope safe programs and their proofs. In: Bertot, Y. and Vafeiadis, V. (eds.) Proceedings of the 6th Conference on Certified Programs and Proofs (CPP’17), ACM, 195–207.Google Scholar
Ambler, S. and Crole, R.L. (1999). Mechanized operational semantics via (co)induction. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C. and Théry, L. (eds.) Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’99), Lecture Notes in Computer Science, vol. 1690, Springer, 221–238.CrossRefGoogle Scholar
Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A. and Wang, Y. (2014). Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning 7 (2) 1–89.Google Scholar
Baelde, D., Gacek, A., Miller, D., Nadathur, G. and Tiu, A. (2007). The Bedwyr system for model checking over syntactic expressions. In: Proceedings of the 21st Conference on Automated Deduction (CADE), Lecture Notes in Computer Science, vol. 4603, Springer, 391–397.CrossRefGoogle Scholar
Bengtson, J. and Parrow, J. (2009). Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science 5 (2) 1–36.CrossRefGoogle Scholar
Bengtson, J., Parrow, J. and Weber, T. (2016). Psi-calculi in Isabelle. Journal of Automated Reasoning 56 (1) 1–47.CrossRefGoogle Scholar
Benton, N., Hur, C., Kennedy, A. and McBride, C. (2012). Strongly typed term representations in coq. Journal of Automated Reasoning 49 (2) 141–159.CrossRefGoogle Scholar
Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kuncar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D. (2017). Foundational (co)datatypes and (co)recursion for higher-order logic. In: Dixon, C. and Finger, M. (eds.) Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS’17), Lecture Notes in Computer Science, vol. 10483, Springer, 3–21.Google Scholar
Cave, A. and Pientka, B. (2012). Programming with binders and indexed data-types. In: Proceedings of the 39th Symposium on Principles of Programming Languages (POPL’12), ACM Press, 413–424.Google Scholar
Cave, A. and Pientka, B. (2013). First-class substitutions in contextual type theory. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’13), ACM Press, 15–24.Google Scholar
Cave, A. and Pientka, B. (2015). A case study on logical relations using contextual types. In: Cervesato, I. and Chaudhuri, K. (eds.) Proceedings of the 10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’15), Electronic Proceedings in Theoretical Computer Science, 18–33.Google Scholar
Cave, A. and Pientka, B. (2018). Mechanizing proofs with logical relations – Kripke-style. Mathematical Structures in Computer Science, 28 (Special Issue 9) 1606–1638.CrossRefGoogle Scholar
Chaudhuri, K. (2018). A two-level logic perspective on (simultaneous) substitutions. In Andronick, J. and Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8–9, 2018, ACM, 280–292.CrossRefGoogle Scholar
Chaudhuri, K., Cimini, M. and Miller, D. (2015). A lightweight formalization of the metatheory of bisimulation-up-to. In Leroy, X. and Tiu, A. (eds.) Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP 2015), Mumbai, India, January 15–17, 2015, ACM, 157–166.Google Scholar
Cheney, J. and Momigliano, A. (2017). αcheck: A mechanized metatheory model checker. TPLP 17 (3) 311–352.Google Scholar
Crary, K. and Harper, R. (2007). Syntactic logical relations for polymorphic and recursive types. Electronic Notes in Theoretical Computer Science 172 259–299.CrossRefGoogle Scholar
Felty, A.P. and Momigliano, A. (2012). Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. Journal of Automated Reasoning 48 (1) 43–105.CrossRefGoogle Scholar
Ford, J. and Mason, I.A. (2003). Formal foundations of operational semantics. Higher-Order and Symbolic Computation 16 (3) 161–202.CrossRefGoogle Scholar
Ghica, D.R. and McCusker, G. (2000). Reasoning about idealized ALGOL using regular languages. In: Montanari, U., Rolim, J.D.P. and Welzl, E. (eds.) Proceedings of the 27th International Colloquium, Automata, Languages and Programming (ICALP 2000), Lecture Notes in Computer Science, vol. 1853, Springer, 103–115.Google Scholar
Giménez, E. (1996). Un Calcul de Constructions Infinies et son application à la vérification de systèmes communicants. PhD thesis, Ecole Normale Supérieure de Lyon, Thèse d’université.Google Scholar
Harper, R., Honsell, F. and Plotkin, G. (1993). A framework for defining logics. Journal of the ACM 40 (1) 143–184.CrossRefGoogle Scholar
Hirschkoff, D. (1997). A full formalisation of pi-calculus theory in the calculus of constructions. In: Gunter, E.L. and Felty, A.P. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’97), Lecture Notes in Computer Science, vol. 1275, Springer, 153–169.CrossRefGoogle Scholar
Honsell, F., Miculan, M. and Scagnetto, I. (2001). Π-calculus in (co)inductive type theories. Theoretical Computer Science 2 (253) 239–285.CrossRefGoogle Scholar
Howe, D.J. (1996). Proving congruence of bisimulation in functional programming languages. Information and Computation 124 (2) 103–112.CrossRefGoogle Scholar
Jacob-Rao, R., Pientka, B. and Thibodeau, D. (2018). Index-stratified types. In: Kirchner, H. (ed.) Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD’18), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 19:1–19:17.Google Scholar
Laforgue, P. and Régis-Gianas, Y. (2017). Copattern matching and first-class observations in OCaml, with a macro. In: Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP’17, 97–108.CrossRefGoogle Scholar
Lassen, S. B. (1998). Relational Reasoning About Functions and Nondeterminism. PhD thesis, Department of Computer Science, University of Aarhus.Google Scholar
Lee, D. K., Crary, K. and Harper, R. (2007). Towards a mechanized metatheory of Standard ML. In: Proceedings of the 34th Symposium on Principles of Programming Languages (POPL’07), ACM Press, 173–184.Google Scholar
Lenglet, S. and Schmitt, A. (2018). Hoπ in coq. In: Andronick, J. and Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8–9, 2018, ACM, 252–265.Google Scholar
Mason, I. and Talcott, C. (1991). Equivalence in functional languages with effects. Journal of Functional Programming 1 (03) 287–327.CrossRefGoogle Scholar
McDowell, R. and Miller, D. (1997). A logic for reasoning with higher-order abstract syntax. In: Winskel, G. (eds.) Proceedings of the 12th Symposium on Logic in Computer Science, IEEE Computer Society Press, 434–445.Google Scholar
McDowell, R., Miller, D. and Palamidessi, C. (1996). Encoding transition systems in sequent calculus: Preliminary report. Electronic Notes in Theoretical Computer Science, 3 138–152.CrossRefGoogle Scholar
McLaughlin, C., McKinna, J. and Stark, I. (2018). Triangulating context lemmas. In: Andronick, J. and Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), Los Angeles, CA, USA, January 8–9, 2018, ACM, 102–114.Google Scholar
Miller, D. and Nadathur, G. (2012). Programming with Higher-Order Logic, 1st edition, Cambridge University Press, New York, NY, USA.CrossRefGoogle Scholar
Miller, D. and Palamidessi, C. (1999). Foundational aspects of syntax. ACM Computing Surveys 31 (3es) 1–7.CrossRefGoogle Scholar
Miller, D. and Tiu, A. (2005). A proof theory for generic judgments. ACM Transactions on Computational Logic 6 (4) 749–783.CrossRefGoogle Scholar
Milner, R. (1977). Fully abstract models of typed -calculi. Theoretical Computer Science 4 (1) 1–22.CrossRefGoogle Scholar
Momigliano, A. (2012). A supposedly fun thing I may have to do again: A HOAS encoding of Howe’s method. In: Proceedings of the 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP’12), ACM, 33–42.CrossRefGoogle Scholar
Momigliano, A., Ambler, S. and Crole, R. L. (2002). A Hybrid encoding of Howe’s method for establishing congruence of bisimilarity. Electronic Notes in Theoretical Computer Science 70 (2) 60–75.CrossRefGoogle Scholar
Momigliano, A. and Tiu, A. (2003). Induction and co-induction in sequent calculus. In: Coppo, M., Berardi, S. and Damiani, F. (eds.) Post-Proceedings of TYPES 2003, Lecture Notes in Computer Science, vol. 3085, 293–308.Google Scholar
Nanevski, A., Pfenning, F. and Pientka, B. (2008). Contextual modal type theory. ACM Transactions on Computational Logic 9 (3) 1–49.CrossRefGoogle Scholar
Oury, N. (2008). Coinductive types and type preservation. Message on the coq-club mailing list.Google Scholar
Parrow, J., Borgström, J., Raabjerg, P. and Pohjola, J.Å. (2014). Higher-order psi-calculi. Mathematical Structures in Computer Science 24 (2) 1–36.CrossRefGoogle Scholar
Pfenning, F. (1997). Computation and deduction. Accessed January 31st, 2018.Google Scholar
Pfenning, F. and Schürmann, C. (1999). System description: Twelf – A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Lecture Notes in Artificial Intelligence, vol. 1632, Springer, 202–206.CrossRefGoogle Scholar
Pientka, B. (2005). Verifying termination and reduction properties about higher-order logic programs. Journal of Automated Reasoning 34 (2) 179–207.CrossRefGoogle Scholar
Pientka, B. (2008). A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: Proceedings of the 35th Symposium on Principles of Programming Languages (POPL’08), ACM Press, 371–382.CrossRefGoogle Scholar
Pientka, B. (2013). An insider’s look at LF type reconstruction: Everything you never wanted to know. Journal of Functional Programming 23 (1) 1–37.CrossRefGoogle Scholar
Pientka, B. and Abel, A. (2015). Structural recursion over contextual objects. In Altenkirch, T. (ed.) Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA’15), Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl, 273–287.Google Scholar
Pientka, B. and Cave, A. (2015). Inductive Beluga: Programming proofs (system description). In: Felty, A.P. and Middeldorp, A. (eds.) Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Computer Science, vol. 9195, Springer, 272–281.Google Scholar
Pientka, B. and Dunfield, J. (2008). Programming with proofs and explicit contexts. In: Antoy, S. and Albert, E. (eds.) Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15–17, 2008, Valencia, Spain, ACM, 163–173.CrossRefGoogle Scholar
Pientka, B. and Dunfield, J. (2010). Beluga: A framework for programming and reasoning with deductive systems (System Description). In: Giesl, J. and Haehnle, R. (eds.) Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR’10), Lecture Notes in Artificial Intelligence, vol. 6173, Springer, 15–21.Google Scholar
Pitts, A.M. (1997). Operationally based theories of program equivalence. In: Dybjer, P. and Pitts, A.M. (eds.) Semantics and Logics of Computation, Cambridge University Press, 241–298.CrossRefGoogle Scholar
Pitts, A.M. (2005). Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, chapter 7, The MIT Press, 245–289.Google Scholar
Pitts, A.M. (2011). Howe’s method for higher-order languages. In Sangiorgi, D. and Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science, vol. 52, chapter 5, Cambridge University Press, 197–232.CrossRefGoogle Scholar
Thibodeau, D., Cave, A. and Pientka, B. (2016). Indexed codata. In: Garrigue, J., Keller, G. and Sumii, E. (eds.) Proceedings of the 21st International Conference on Functional Programming (ICFP’16), ACM, 351–363.Google Scholar
Tiu, A. and Miller, D. (2010). Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Transactions on Computational Logic 11 (2) 1–35.CrossRefGoogle Scholar
Tiu, A. and Momigliano, A. (2012). Cut elimination for a logic with induction and co-induction. Journal of Applied Logic 10 (4) 330–367.CrossRefGoogle Scholar