zbMATH — the first resource for mathematics

\(\mathrm{HO}\pi\) in Coq. (English) Zbl 07356968
Summary: We present a formalization of \(\mathrm{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.
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Full Text: DOI
[1] Ambler, S.; Crole, RL; Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin-Mohring, C.; Théry, L., Mechanized operational semantics via (co)induction, TPHOLs’99, Volume 1690 of Lecture Notes in Computer Science, 221-238 (1999), Nice: Springer, Nice · Zbl 0954.68093
[2] Anand, A.; Rahli, V.; Klein, G.; Gamboa, R., Towards a formally verified proof assistant, ITP 2014, Volume 8558 of Lecture Notes in Computer Science, 27-44 (2014), Vienna: Springer, Vienna · Zbl 1416.68146
[3] 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) · Zbl 1152.68516
[4] Aydemir, B.E., Weirich, S.: LNgen: tool support for locally nameless representations. Technical report, University of Pennsylvania (2010)
[5] 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) · Zbl 1451.68315
[6] Bengtson, J.; Parrow, J., Formalising the pi-calculus using nominal logic, Log. Methods Comput. Sci., 5, 2, 16 (2009) · Zbl 1168.68030
[7] Bird, RS; Paterson, R., De Bruijn notation as a nested datatype, J. Funct. Program., 9, 1, 77-91 (1999) · Zbl 0926.68025
[8] Bucalo, A.; Honsell, F.; Miculan, M.; Scagnetto, I.; Hofmann, M., Consistency of the theory of contexts, J. Funct. Program., 16, 3, 327-372 (2006) · Zbl 1092.68022
[9] Cervesato, I.; Pfenning, F., A linear logical framework, Inf. Comput., 179, 1, 19-75 (2002) · Zbl 1031.03056
[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) · Zbl 1100.68548
[11] Charguéraud, A.: LN: locally nameless representation with cofinite quantification. http://www.chargueraud.org/softs/ln/ · Zbl 1260.68368
[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) · Zbl 1260.68368
[14] Ciaffaglione, A.; Scagnetto, I., Mechanizing type environments in weak HOAS, Theor. Comput. Sci., 606, 57-78 (2015) · Zbl 1332.68202
[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) · Zbl 0985.68524
[16] de Bruijn, NG, 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) · Zbl 0253.68007
[17] Despeyroux, J.; van Leeuwen, J.; Watanabe, O.; Hagiya, M.; Mosses, PD; Ito, T., A higher-order specification of the pi-calculus, IFIP TCS 2000, Volume 1872 of Lecture Notes in Computer Science, 425-439 (2000), New York: Springer, New York
[18] Despeyroux, J.; Felty, AP; Hirschowitz, A.; Dezani-Ciancaglini, M.; Plotkin, GD, Higher-order abstract syntax in coq, TLCA ”95, Volume 902 of Lecture Notes in Computer Science, 124-138 (1995), New York: Springer, New York
[19] Gay, SJ; Boulton, Richard J.; Jackson, Paul B., A framework for the formalisation of pi calculus type systems in Isabelle/HOL, TPHOLs 2001, 217-232 (2001), Edinburgh: Springer, Edinburgh · Zbl 1005.68531
[20] Gordon, AD, Bisimilarity as a theory of functional programming, Electron. Notes Theor. Comput. Sci., 1, 232-252 (1995) · Zbl 0910.68118
[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) · Zbl 0883.03012
[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) · Zbl 1195.68071
[25] Honsell, F.; Miculan, M.; Scagnetto, I., pi-calculus in (co)inductive-type theory, Theor. Comput. Sci., 253, 2, 239-285 (2000) · Zbl 0956.68095
[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) · Zbl 1268.68048
[27] Howe, DJ, Proving congruence of bisimulation in functional programming languages, Inf. Comput., 124, 2, 103-112 (1996) · Zbl 0853.68073
[28] Gabbay, MJ, The pi-calculus in FM, Thirty Five Years Autom. Math., 28, 247-269 (2003) · Zbl 1063.68073
[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) · Zbl 1374.68338
[31] Lenglet, S.; Schmitt, A.; Andronick, J.; Felty, AP, HO \(\pi\) in Coq, CPP 2018, 252-265 (2018), Copenhagen: ACM, Copenhagen
[32] Lenglet, S.; Schmitt, A.; Stefani, J-B, Characterizing contextual equivalence in calculi with passivation, Inf. Comput., 209, 11, 1390-1433 (2011) · Zbl 1251.68160
[33] Maksimovic, P.; Schmitt, A.; Urban, C.; Zhang, X., Hocore in Coq, ITP 2015, Volume 9236 of Lecture Notes in Computer Science, 278-293 (2015), Nanjing: Springer, Nanjing · Zbl 1465.68196
[34] McKinna, J.; Pollack, R.; Bezem, M.; Groote, JF, Pure type systems formalized, TLCA ’93, Volume 664 of Lecture Notes in Computer Science, 289-305 (1993), New York: Springer, New York · Zbl 0835.68068
[35] Melham, TF, 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) · Zbl 1367.03059
[37] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes. I, Inf. Comput., 100, 1, 1-40 (1992) · Zbl 0752.68036
[38] Mohamed, O.A.: Mechanizing a pi-calculus equivalence in hol. In: TPHOL 95, pp. 1-16. Springer (1995) · Zbl 1063.68600
[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) · Zbl 1342.68239
[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) · Zbl 1400.68142
[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.; Ganzinger, H., System description: Twelf—a meta-logical framework for deductive systems, CADE 99, Volume 1632 of Lecture Notes in Computer Science, 202-206 (1999), New York: Springer, New York
[44] Pientka, B.; Dunfield, J.; Giesl, J.; Hähnle, R., Beluga: a framework for programming and reasoning with deductive systems (system description), IJCAR 2010, Volume of 6173 Lecture Notes in Computer Science, 15-21 (2010), Edinburgh: Springer, Edinburgh · Zbl 1291.68366
[45] Pitts, AM, Nominal logic, a first order theory of names and binding, Inf. Comput., 186, 2, 165-193 (2003) · Zbl 1056.03014
[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) · Zbl 1268.68053
[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) · Zbl 1096.68679
[48] Sangiorgi, D., Bisimulation for higher-order process calculi, Inf. Comput., 131, 2, 141-178 (1996) · Zbl 0876.68042
[49] Sangiorgi, D.; Walker, D., The Pi-Calculus: A Theory of Mobile Processes (2001), Cambridge: Cambridge University Press, Cambridge · Zbl 0981.68116
[50] Stark, K.; Schäfer, S.; Kaiser, J.; Mahboubi, A.; Myreen, MO, Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions, CPP 19, 166-180 (2019), Copenhagen: ACM, Copenhagen
[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) · Zbl 1430.68418
[53] Urban, C., Nominal techniques in Isabelle/HOL, J. Autom. Reason., 40, 4, 327-356 (2008) · Zbl 1140.68061
[54] Urban, C., Berghofer, S., Kaliszyk, C.: Nominal 2. Archive of Formal Proofs (2013). http://isa-afp.org/entries/Nominal2.html, Formal proof development
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.