[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A Formalization of a Concurrent Object Calculus up to α-Conversion

  • Conference paper
Automated Deduction - CADE-17 (CADE 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1831))

Included in the following conference series:

Abstract

We experiment a method for representing a concurrent object calculus in the Calculus of Inductive Constructions. Terms are first defined in de Bruijn style, then names are re-introduced in binders. The terms of the calculus are formalized in the mechanized logic by suitable subsets of the de Bruijn terms; namely those whose de Bruijn indices are relayed beyond the scene. The α-equivalence relation is the Leibnitz equality and the substitution functions can be defined as sets of partial rewriting rules on these terms. We prove induction schemes for both the terms and some properties of the calculus which internalize the re-naming of bound variables. We show that despite the fact the terms which formalize the calculus are not generated by a last fixed point relation, we can prove the desired inversion lemmas. We formalize the computational part of the semantic and a simple type system of the calculus. Finally, we prove a subject reduction theorem and see that the specifications and proofs have the nice feature of not mixing de Bruijn technical manipulations with real proofs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  2. Barras, B.: Coq en Coq. Mémoire du DEA informatique, mathématiques et applications, École Polytechnique, 1995. INRIA research report RR-3026 (October 1996)

    Google Scholar 

  3. Bertot, J., Bertot, Y., Coscoy, Y., Goguen, H., Montagnac, F.: User uide to the CtCoq proof environment, Inria technical report, RT-0210 (October 1997)

    Google Scholar 

  4. de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. In: Geuvers, J.H., Nederpelt, R.P., de Vrijer, R.C. (eds.) Selected Papers on Automath, Studies in Logic vol. 133, pp. 375–388. Springer, Heidelberg (1994) (reprinted)

    Google Scholar 

  5. Despeyroux, J.: A higher-order specification of the pi-calculus. Presented at the Modelisation and Verification seminar, Marseille (December 1998); submitted for publication, March

    Google Scholar 

  6. Despeyroux, J., Hirschowitz, A.: Higher-order syntax and induction in Coq. In: Pfenning, F. (ed.) LPAR 1994. LNCS (LNAI), vol. 822, pp. 159–173. Springer, Heidelberg (1994) Also appears as INRIA Research Report RR-2292 (June 1994)

    Google Scholar 

  7. Miculan, M., Honsell, F., Scagnetto, I.: Pi calculus in (co)inductive type theories. Technical report, Universita’ di Udine (September 1998)

    Google Scholar 

  8. Gordon, A., Hankin, P.: A concurrent object calculus: reduction and typing. In: Proceedings of the HLCL 1998 Conference. Elsevier ENTCS, Amsterdam (1998)

    Google Scholar 

  9. Gillard, G.: A full formalization of a concurrent object cal-culus up to alpha-conversion (January 2000); draft, Available at ftp://ftp-sop.inria.fr/certilab/ps/conc_calculus.ps

  10. Gordon, A.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 413–425. Springer, Heidelberg (1994)

    Google Scholar 

  11. Henry_Greard, L.: A proof of type preservation for the pi-calculus in Coq. Research Report RR-3698, Inria (December 1998); Also available in the Coq Contrib library

    Google Scholar 

  12. Hirschkoff, D.: A full formalization of pi-calculus theory in the Calculus of Constructions. In: Felty, A., Gunter, E. (eds.) Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Murray Hill, New Jersey (August 1997)

    Google Scholar 

  13. McKinna, J., Pollack, R.: Pure Type Sytems formalized. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 289–305. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  14. Milner, R., Parrow, R., Walker, J.: A calculus of mobile processes (part I and II). Information and Computation 100, 1–77 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  15. Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, University Paris VII (Mai 1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Sophia Antipolis,  

    Guillaume Gillard

Authors
  1. Guillaume Gillard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Toyota Technological Institute at Chicago, 1427 E. 60th Street, 60637, Chicago, Illinois

    David McAllester

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gillard, G. (2000). A Formalization of a Concurrent Object Calculus up to α-Conversion. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_33

Download citation

  • DOI: https://doi.org/10.1007/10721959_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67664-5

  • Online ISBN: 978-3-540-45101-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation