Gérard Boudol

Welcome to my home page. I am a Research Director at INRIA, Sophia-Antipolis, within the MIMOSA project. My research interests include theory of concurrency (process algebras, verification, ``true concurrency''), lambda-calculus, models of higher-order and mobile distributed systems, semantics of objects. I am also interested in programming languages design and semantics, type theories, logics.

Address

INRIA

2004, Route des Lucioles

B.P. 93

06902 Sophia Antipolis Cedex

FRANCE

Tel: (33) (0)4 92 38 79 40

Fax: (33) (0)4 92 38 79 98

Email: Gerard.Boudol@sophia.inria.fr

Some Links

The page Calculi for Mobile Processes provides information and links related to research on the theory of mobile systems. See also Xudong Guan's Mobile Ambients page. I use very frequently Hypatia, a directory of researchers in Computer Science and Pure Mathematics, The Collection of Computer Science Bibliographies, and NCSTRL, the Networked Computer Science Technical Reference Library. To see the home page of the European Association for Theoretical Computer Science, of which I am a member, hit EATCS. Some useful email forums are concurrency, types and moca (mobile calculi).

Some Publications

Below you will find a list of publications. For the items marked with a square, a PostScript is available. Please ask me if you wish to have a copy of some item marked with a circle, where you can only browse an Abstract. I have classified these papers according to the following entries: semantics of objects, security, pi-calculus and its variants, lambda-calculus, concurrency and verification, term rewriting systems.

The recursive record semantics of objects revisited, submitted for publication. A preliminary version of this work appeared at ESOP 2001 (as part of ETAPS 2001), Lecture Notes in Computer Science (LNCS) Vol 2028 (2001), 269-283).
[Abstract, PostScript, .ps.gz]

An interpretation of extensible objects, with S. Dal-Zilio, Fundamentals of Computation Theory (FCT'99), Lecture Notes in Computer Science (LNCS) Vol 1684 (1999), 148-160.
[Abstract, PostScript, .ps.gz]

Non-interference for concurrent programs, with I. Castellani, submitted for publication. This is an extended version of a paper accepted at ICALP 2001.
[Abstract, PostScript, .ps.gz]

See also: On the semantics of the call-by-name CPS transform, Some chemical abstract machines.

The receptive distributed pi-calculus, with R. Amadio and C. Lhoussaine, INRIA Research Report 4080 (November 2000). This work was presented at the Mobile Object Systems (MOS) workshop on Programming Languages for Wide Area Networks (MOS'99), Lisbon, June 14, 1999. An extended abstract appeared in the proceedings of the FST-TCS'99 Conference, Lecture Notes in Computer Science (LNCS) Vol 1738 (1999), 304-315.
[Abstract, PostScript, .ps.gz]

Lambda-calculus, multiplicities and the pi-calculus, with C. Laneve, in Proof, Language, and Interaction, Essays in Honour of Robin Milner (G. Plotkin, C. Stirling, M. Tofte Eds.), Foundations of Computing series, The MIT Press (2000), 659-689.
[Abstract]

Typing the use of resources in a concurrent calculus, ASIAN'97, the Asian Computing Science Conference, Kathmandu, Nepal, LNCS 1345 (1997), 239-253.
[Abstract, PostScript, .ps.gz]

The pi-calculus in direct style, POPL'97 (1997), 228-241.
[Abstract, Preliminary version PostScript, .ps.gz]
An extended version of the POPL'97 paper has appeared in Higher-Order and Symbolic Computation, Vol 11 (1998) 177-208. See also S. Dal-Zilio's PhD Thesis - The Blue Calculus: Types and Objects.

Asynchrony and the pi-calculus, INRIA Research Report 1702 (May 1992).
[Abstract, PostScript, .ps.gz]

See also: Lambda-calculus, multiplicities and the pi-calculus, The pi-calculus in direct style, Some chemical abstract machines.

On the semantics of the call-by-name CPS transform, Theoretical Computer Science (TCS) Vol. 234 (2000), 309-321
[Abstract]

A semantics for lambda calculi with resources, with P.-L. Curien and C. Lavatelli, in Mathematical Structures in Comput. Sci. (MSCS) Vol. 9 (1999), 437-482.
[Abstract]

The discriminating power of multiplicities in the lambda-calculus, with C. Laneve, in Information and Computation Vol. 126, No. 1 (1996), 83-102.
[Abstract]

Full abstraction for a lambda-calculus with resources and convergence testing, with C. Lavatelli, CAAP'96, LNCS 1059 (1996), 302-316.
[Abstract]

Termination, deadlock and divergence in the lambda-calculus with multiplicities, with C. Laneve, MFPS'95, Electronic Notes in Theoretical Computer Science (ENTCS ), Vol. 1 (1995).
[Abstract]

Lambda-calculi for (strict) parallel functions, in Information and Computation Vol. 108, No. 1 (1994), 51-127.
[Abstract]

The lambda-calculus with multiplicities, INRIA Research Report 2025 (September 1993).
[Abstract, PostScript, .ps.gz ]

Flow models of distributed computations: three equivalent semantics for CCS, with I. Castellani, in Information and Computation Vol. 114, N0 2 (1994), 247-314.
[Abstract]

A theory of processes with localities, with I. Castellani, M. Hennessy and A. Kiehn, in Formal Aspects of Computing (FAC), Vol 6 (1994), 165-200.
[Abstract]

Some chemical abstract machines, in A Decade of Concurrency - Reflections and Perspectives, Lecture Notes in Computer Science (LNCS) Vol 803 (1994), 92-123.
[Abstract, PostScript, .ps.gz]

Observing localities, with I. Castellani, M. Hennessy and A. Kiehn, in Theoretical Computer Science (TCS) Vol. 114 (1993), 31-61.
[Abstract]

Graphical vs logical specifications, with K.G. Larsen, in Theoretical Computer Science (TCS ) Vol. 106 (1992), 3-20.
[Abstract]

The chemical abstract machine, with G. Berry, in Theoretical Computer Science (TCS ) Vol. 96 (1992), 217-248.
[Abstract]

Atomic actions, in EATCS Bulletin Vol. 38 (1989), 136-144.
[Abstract, PostScript, .ps.gz]

A non-interleaving semantics for CCS based on proved transitions, with I. Castellani, in Fundamentae Informaticae XI (1988), 433-453.
[Abstract]

Concurrency and atomicity, with I. Castellani, in Theoretical Computer Science (TCS ) Vol. 59 (1988), 25-84.
[Abstract]

Experiment with AUTO and AutoGraph on a simple case of a sliding window protocol, with R. De Simone and D. Vergamini, INRIA Research Report 870 (July 1988).
[Abstract]

Petri nets and algebraic calculi of processes, with G. Roucairol and R. De Simone, in Advances in Petri Nets, Lecture Notes in Computer Science (LNCS) Vol 222 (1985), 41-58.
[Abstract]

Notes on algebraic calculi of processes, in Logics and Models of Concurrent Systems, NATO ASI Series F-13 (1985), 261-303.
[Abstract]

Algèbre de processus et synchronisation, with D. Austry, in Theoretical Computer Science (TCS) Vol. 30 (1984), 91-131.
[Abstract]

Computational semantics of term rewriting systems, in Algebraic Methods in Semantics (M. Nivat & J.C. Reynolds, Eds), Cambridge University Press (1985), 169-236.
[Abstract]

Recursion induction principle revisited, with L. Kott, in Theoretical Computer Science (TCS) Vol. 22 (1983), 135-173.
[Abstract]