Top

Journal of Automated Reasoning

Published in:

14-09-2020

HO\(\pi \) in Coq

Authors: Guillaume Ambal, Sergueï Lenglet, Alan Schmitt

Published in: Journal of Automated Reasoning | Issue 1/2021

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We present a formalization of HO\(\pi \) in Coq, a process calculus where messages carry processes. Such a higher-order calculus features two very different kinds of binder: process input, similar to \(\lambda \)-abstraction, and name restriction, whose scope can be expanded by communication. For the latter, we compare four approaches to represent binders: locally nameless, de Bruijn indices, nominal, and Higher-Order Abstract Syntax. In each case, we formalize strong context bisimilarity and prove it is compatible, i.e., closed under every context, using Howe’s method, based on several proof schemes we developed in a previous paper.

previous article Formalization of the Poincaré Disc Model of Hyperbolic Geometry

next article Building Strategies into QBF Proofs

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

In the code, we define coercions from respectively and to

Charguéraud [13] denotes this property as locally closed, but we prefer to use a different term, as our notion of closed process refers to process variables and not names.

Regular HOAS, which relies on functions from terms to terms, cannot be used in Coq to define the syntax of some object language L, as inductive types of the form \((L \rightarrow L) \rightarrow L\) are not allowed [18].

Process functions can be seen as contexts, since they map name to terms.

Ambler, S., Crole, R.L.: Mechanized operational semantics via (co)induction. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Théry, L. (eds.) TPHOLs’99, Volume 1690 of Lecture Notes in Computer Science, pp. 221–238. Springer, Nice (1999)

Anand, A., Rahli, V.: Towards a formally verified proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014, Volume 8558 of Lecture Notes in Computer Science, pp. 27–44. Springer, Vienna (2014)

Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the PoplMark challenge. In: TPHOLs, pp. 50–65 (2005)

Aydemir, B.E., Weirich, S.: LNgen: tool support for locally nameless representations. Technical report, University of Pennsylvania (2010)

Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1–89 (2014)MathSciNetMATH

Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci. 5(2), 16 (2009)MATHCrossRef

Bird, R.S., Paterson, R.: De Bruijn notation as a nested datatype. J. Funct. Program. 9(1), 77–91 (1999)MathSciNetMATHCrossRef

Bucalo, A., Honsell, F., Miculan, M., Scagnetto, I., Hofmann, M.: Consistency of the theory of contexts. J. Funct. Program. 16(3), 327–372 (2006)MathSciNetMATHCrossRef

Cervesato, I., Pfenning, F.: A linear logical framework. Inf. Comput. 179(1), 19–75 (2002)MathSciNetMATHCrossRef

10.

Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A concurrent logical framework II: examples and applications. Technical report CMU-CS-02-102, Carnegie Mellon University (2002)

11.

Charguéraud, A.: LN: locally nameless representation with cofinite quantification. http://www.chargueraud.org/softs/ln/

12.

Charguéraud, A.: TLC: a non-constructive library for Coq. http://www.chargueraud.org/softs/tlc/

13.

Charguéraud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363–408 (2012)MathSciNetMATHCrossRef

14.

Ciaffaglione, A., Scagnetto, I.: Mechanizing type environments in weak HOAS. Theor. Comput. Sci. 606, 57–78 (2015)MathSciNetMATHCrossRef

15.

Dal Zilio, S.: Mobile processes: a commented bibliography. In: MOVEP’2K—4th Summer school on Modelling and Verification of Parallel Processes, Volume 2067 of Lecture Notes in Computer Science, pp. 206–222. Springer (2001)

16.

de Bruijn, N.G.: Lambda calculus notation with nameless dummies: a tool for automatic formula manipulation, with application to the Church–Rosser theorem. Indag. Math. 75(5), 381–392 (1972)MathSciNetMATHCrossRef

17.

Despeyroux, J.: A higher-order specification of the pi-calculus. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) IFIP TCS 2000, Volume 1872 of Lecture Notes in Computer Science, pp. 425–439. Springer, New York (2000)

18.

Despeyroux, J., Felty, A.P., Hirschowitz, A.: Higher-order abstract syntax in coq. In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA ”95, Volume 902 of Lecture Notes in Computer Science, pp. 124–138. Springer, New York (1995)

19.

Gay, S.J.: A framework for the formalisation of pi calculus type systems in Isabelle/HOL. In: Boulton, Richard J., Jackson, Paul B. (eds.) TPHOLs 2001, vol. 2152, pp. 217–232. Springer, Edinburgh (2001)

20.

Gordon, A.D.: Bisimilarity as a theory of functional programming. Electron. Notes Theor. Comput. Sci. 1, 232–252 (1995)MathSciNetMATHCrossRef

21.

Henry-Gréard, L.: Proof of the subject reduction property for a pi-calculus in COQ. Technical report RR-3698, INRIA (1999)

22.

Hirschkoff, D.: A full formalisation of pi-calculus theory in the calculus of constructions. In: Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, vol. 1275, pp. 153–169. Springer (1997)

23.

Hirschkoff, D.: Up to context proofs for the \(\pi \)-calculus in the Coq system. Technical report 97-82, CERMICS (1997)

24.

Hirschkoff, D., Pous, D.: A distribution law for CCS and a new congruence result for the pi-calculus. In: Proceedings of FoSSaCS’07, Volume 4423 of LNCS, pp. 228–242. Springer (2007)

25.

Honsell, F., Miculan, M., Scagnetto, I.: pi-calculus in (co)inductive-type theory. Theor. Comput. Sci. 253(2), 239–285 (2000)MATHCrossRef

26.

Honsell, F., Miculan, M., Scagnetto, I.: The theory of contexts for first order and higher order abstract syntax. Electr. Notes Theor. Comput. Sci. 62, 116–135 (2001)MATHCrossRef

27.

Howe, D.J.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)MathSciNetMATHCrossRef

28.

Gabbay, M.J.: The pi-calculus in FM. Thirty Five Years Autom. Math. 28, 247–269 (2003)MATHCrossRef

29.

Keuchel, S., Weirich, S., Schrijvers, T.: Needle & knot: binder boilerplate tied up. In: ESOP 16, Volume 9632 of Lecture Notes in Computer Science, pp. 419–445. Springer (2016)

30.

Lenglet, S., Schmitt, A.: Howe’s method for contextual semantics. In: Aceto, L., de Frutos-Escrig, D. (eds.) 26th International Conference on Concurrency Theory, CONCUR 2015, Volume 42 of LIPIcs, pp. 212–225. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Madrid, Spain (2015)

31.

Lenglet, S., Schmitt, A.: HO\(\pi \) in Coq. In: Andronick, J., Felty, A.P. (eds.) CPP 2018, pp. 252–265. ACM, Copenhagen (2018)CrossRef

32.

Lenglet, S., Schmitt, A., Stefani, J.-B.: Characterizing contextual equivalence in calculi with passivation. Inf. Comput. 209(11), 1390–1433 (2011)MathSciNetMATHCrossRef

33.

Maksimovic, P., Schmitt, A.: Hocore in Coq. In: Urban, C., Zhang, X. (eds.) ITP 2015, Volume 9236 of Lecture Notes in Computer Science, pp. 278–293. Springer, Nanjing (2015)

34.

McKinna, J., Pollack, R.: Pure type systems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA ’93, Volume 664 of Lecture Notes in Computer Science, pp. 289–305. Springer, New York (1993)

35.

Melham, T.F.: A mechanized theory of the pi-calculus in HOL. Nord. J. Comput. 1(1), 50–76 (1994)

36.

Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749–783 (2005)MathSciNetMATHCrossRef

37.

Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1–40 (1992)MathSciNetMATHCrossRef

38.

Mohamed, O.A.: Mechanizing a pi-calculus equivalence in hol. In: TPHOL 95, pp. 1–16. Springer (1995)

39.

Momigliano, A.: A supposedly fun thing I may have to do again: a HOAS encoding of Howe’s method. In: LFMTP 12, pp. 33–42(2012). ACM, Copenhagen, Denmark

40.

Parrow, J., Borgström, J., Raabjerg, P., Åman Pohjola, J.: Higher-order psi-calculi. Math. Struct. Comput. Sci. First View, 1–37 (2014)MathSciNetMATH

41.

Perera, R., Cheney, J.: Proof-relevant \(\pi \)-calculus: a constructive account of concurrency and causality. Math. Struct. Comput. Sci. 28(9), 1541–1577 (2018)MathSciNetMATH

42.

Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI 88, pp. 199–208. ACM, Atlanta, Georgia, USA (1988)

43.

Pfenning, F., Schürmann, C.: System description: Twelf—a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 99, Volume 1632 of Lecture Notes in Computer Science, pp. 202–206. Springer, New York (1999)

44.

Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010, Volume of 6173 Lecture Notes in Computer Science, pp. 15–21. Springer, Edinburgh (2010)

45.

Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165–193 (2003)MathSciNetMATHCrossRef

46.

Röckl, C.: A first-order syntax for the pi-calculus in isabelle/hol using permutations. Electr. Notes Theor. Comput. Sci. 58(1), 1–17 (2001)MATHCrossRef

47.

Röckl, C., Hirschkoff, D.: A fully adequate shallow embedding of the [pi]-calculus in isabelle/hol with mechanized syntax analysis. J. Funct. Program. 13(2), 415–451 (2003)MATHCrossRef

48.

Sangiorgi, D.: Bisimulation for higher-order process calculi. Inf. Comput. 131(2), 141–178 (1996)MathSciNetMATHCrossRef

49.

Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH

50.

Stark, K., Schäfer, S., Kaiser, J.: Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In: Mahboubi, A., Myreen, M.O. (eds.) CPP 19, pp. 166–180. ACM, Copenhagen (2019)

51.

The Penn PL Club: The Penn locally nameless metatheory library. https://github.com/plclub/metalib

52.

Thibodeau, D., Momigliano, A., Pientka, B.: A case-study in programming coinductive proofs: Howe’s method. http://www.momigliano.di.unimi.it/papers/bhowe.pdf (2016)

53.

Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008)MathSciNetMATHCrossRef

54.

Urban, C., Berghofer, S., Kaliszyk, C.: Nominal 2. Archive of Formal Proofs (2013). http://isa-afp.org/entries/Nominal2.html, Formal proof development

Title: HO in Coq
Authors: Guillaume Ambal
Sergueï Lenglet
Alan Schmitt
Publication date: 14-09-2020
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 1/2021
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-020-09553-0

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner