Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1/2021

14.09.2020

HO\(\pi \) in Coq

verfasst von: Guillaume Ambal, Sergueï Lenglet, Alan Schmitt

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2021

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Vorheriger Artikel Formalization of the Poincaré Disc Model of Hyperbolic Geometry
Nächster Artikel Building Strategies into QBF Proofs

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
In the code, we define coercions from respectively and to
 
2
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.
 
3
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].
 
4
Process functions can be seen as contexts, since they map name to terms.
 
Literatur
1.
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)
2.
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)
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)
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)MathSciNetMATH
6.
Bengtson, J., Parrow, J.: Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci. 5(2), 16 (2009)MATHCrossRef
7.
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)MathSciNetMATHCrossRef
9.
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.
12.
13.
14.
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.
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.
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.
37.
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.
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.
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.
52.
53.
54.
Metadaten
Titel
HO in Coq
verfasst von
Guillaume Ambal
Sergueï Lenglet
Alan Schmitt
Publikationsdatum
14.09.2020
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-020-09553-0