Abstract
We present a Natural Deduction proof system for the propositional modal π-calculus, and its formalization in the Calculus of Inductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in presence of recursive constructors, the encoding of modal (sequent-style) rules and of context sensitive grammars. The formalization can be used in the system Coq, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the π-calculus. The techniques we adopt can be readily ported to other languages and proof systems featuring similar problematic issues.
Work partially supported by Italian MURST-97 grant Techniche formali...
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Avron, F. Honsell, M. Miculan, and C. Paravano. Encoding modal logics in Logical Frameworks. Studia Logica, 60(1):161–208, Jan. 1998.
A. Church. A formulation of the simple theory of types. JSL, 5:56–68, 1940.
G. D’Agostino, M. Hollenberg. Logical questions concerning the π-calculus: interpolation, Lyndon, and Loś-Tarski. To be published in the JSL, 1999.
J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order syntax in Coq. In Proc. of TLCA’95. LNCS 902, Springer-Verlag, 1995.
G. Gentzen. Investigations into logical deduction. In M. Szabo, ed., The collected papers of Gerhard Gentzen, pages 68–131. North Holland, 1969.
R. Harper, F. Honsell, and G. Plotkin.A framework for defining logics. J. ACM, 40(1):143–184, Jan. 1993.
D. Kozen. Results on the propositional π-calculus. TCS, 27:333–354, 1983.
Z. Luo, R. Pollack, et al. The LEGO proof assistant. Department of Computer Science, University of Edinburgh. http://www.dcs.ed.ac.uk/home/lego
L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Proc. of TYPES’93, LNCS 806, pages 213–237. Springer-Verlag, 1994.
P. Martin-Löf. On the meaning of the logical constants and the justifications of the logic laws. TR 2, Dip. di Matematica, Università di Siena, 1985.
M. Miculan. Encoding the π-calculus in Coq. Available at http://www.dimi.uniud.it/~miculan/mucalculus
M. Miculan. Encoding Logical Theories of Programs. PhD thesis, Dipartimento di Informatica, Università di Pisa, Italy, Mar. 1997.
D. Miller. Unification of Simply Typed Lambda-Terms as Logic Programming. In Proc. of Eighth Intl. Conf. on Logic Programming. MIT, 1991.
B. Nordström, K. Petersson, and J.M. Smith. Martin-Löf’s type theory. In Handbook of Logic in Computer Science. Oxford University Press, 1992.
C. Stirling, and D. Walker. Local model checking in the modal π-calculus. Theoretical Computer Science, 89:161–177, 1983.
I. Walukiewicz. Completeness of Kozen’s axiomatisation. In D. Kozen, editor, Proc. 10th LICS, pages 14–24, June 1995. IEEE.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miculan, M. (1999). Formalizing a Lazy Substitution Proof System for π-Calculus in the Calculus of Inductive Constructions. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds) Automata, Languages and Programming. Lecture Notes in Computer Science, vol 1644. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48523-6_52
Download citation
DOI: https://doi.org/10.1007/3-540-48523-6_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66224-2
Online ISBN: 978-3-540-48523-0
eBook Packages: Springer Book Archive