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, security. 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 50 29

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, and Jonathan Bowen's Concurrent Systems. This is part of the WWW Virtual Library on Computing (other topics may be found here). I use frequently the DBLP bibliographical database, the Scientific Literature Digital Library (CiteSeer), 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 the list of (what I consider) my main publications. For the items marked with a square, a PostScript and/or a pdf 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, mobility (especially pi-calculus and its variants), lambda-calculus, concurrency and verification, term rewriting systems.

See also: Recursion in the call-by-value lambda-calculus, Safe recursive boxes.

The recursive record semantics of objects revisited, Journal of Functional Programming (JFP), Vol. 14, No. 3 (May 2004) 263-315. Preliminary journal version in INRIA Research Report 4199 (June 2001).
[Abstract]
Note: A preliminary conference version of this work appeared at ESOP 2001 (as part of ETAPS 2001), Lecture Notes in Computer Science (LNCS) Vol 2028 (2001), 269-283. The type systems in these two versions are different, as explained in the journal version.

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]

Access-control and declassification, with M. Kolundzija, MMM-ACNS'07 Conference, Communications in Computer and Information Science, Vol. 1 (2007).
[Abstract, .pdf]

On declassification and the non-disclosure policy, with A. Almeida Matos, accepted for publication in the J. of Computer Security, March 2007.
[Abstract, .pdf]
Note: Although this paper has the same title as the CSFW'05 one, it deals with a different type and effect system, namely the one of the paper "On typing information flow."

Typing non-interference for reactive programs, with A. Matos and I. Castellani, INRIA RR-5594, June 2005. Revised version published in the Journal of Logic and Algebraic Programming (special issue on programming language interference and dependence), Vol. 72 (2007) 124-156.
[Abstract, .pdf]

On typing information flow. An extended abstract appeared in the Proceedings of ICTAC'05, Lecture Notes in Computer Science (LNCS) Vol 3722 (2005), 366-380.
[Abstract,.ps.gz, .pdf]

On declassification and the non-disclosure policy, with A. Almeida Matos, May 2005.
[Abstract,.ps.gz, .pdf]
Note: A workshop version of this paper, without proofs, appeared in the proceedings of the Computer Security Foundations Workshop (CSFW'05), June 2005.
[.ps.gz, .pdf]

Non-interference for concurrent programs and thread systems, with I. Castellani, in "Merci, Maurice, A mosaic in honour of Maurice Nivat" (P.-L. Curien, Ed.), Theoretical Computer Science Vol. 281, No. 1 (June 2002) 109-130
[Abstract]
Note: although this paper builds on the next one, it uses a slightly different type system for concurrent programs without scheduling, and presents a more general solution for scheduling sequential threads.

Non-interference for concurrent programs, with I. Castellani, ICALP'2001, Lecture Notes in Computer Science (LNCS) Vol 2076 (2001), 382-395.
[Abstract, PostScript, .ps.gz]

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

A generic membrane model, Global Computing Workshop, Rovereto. Lecture Notes in Computer Science (LNCS) Vol 3267 (2005), 208-222.
[Abstract, pdf]

ULM, a core programming model for global computing, draft (October 2003). An extended abstract of this paper has appeared in the proceedings of the ESOP'04 Conference, Lecture Notes in Computer Science (LNCS) Vol 2986 (2004), 234-248.
[Abstract, pdf, .ps.gz]

The receptive distributed pi-calculus, with R. Amadio and C. Lhoussaine, ACM TOPLAS Vol. 25 No. 5 (2003) 549-577.
A preliminary version has been published as 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]

On message deliverability and non-uniform receptivity, with R. Amadio and C. Lhoussaine, Fundamenta Informaticae Vol. 53 No. 2 (2002), 105-130.
[Abstract, PostScript, .ps.gz]

Models of distribution and mobility: state of the art, with I. Castellani, F. Germain and M. Lacoste. MIKADO Global Computing Project, IST-2001-32222, Deliverable D1.1.1 (August 2002).
[Abstract, pdf]

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: Fair cooperative multithreading, or: Typing termination in a higher-order concurrent imperative language, Lambda-calculus, multiplicities and the pi-calculus, The pi-calculus in direct style, Some chemical abstract machines.

On strong normalization and type inference in the intersection type discipline, to appear in Theoretical Computer Science (June 2007).
[Abstract, pdf]

On type inference in the intersection type discipline, with P. Zimmer, ITRS'04 Workshop (satellite event of ICALP'04), Electronic Notes in Computer Science 136 (2005) 23-42.
[Abstract, pdf, .ps.gz]

Safe recursive boxes, INRIA Research Report 5115 (February 2004).
[Abstract, pdf, .ps.gz]

On strong normalization in the intersection type discipline, TLCA'03, LNCS 2701 (2003), 60-74.
[Abstract, PostScript, .ps.gz]

Recursion in the call-by-value lambda-calculus, with P. Zimmer,Fixed Points in Computer Science Workshop (FICS'02), part of FLoC'02.
[Abstract, PostScript, .ps.gz]

On the semantics of the call-by-name CPS transform, Theoretical Computer Science 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 ]

Fair cooperative multithreading, or: Typing termination in a higher-order concurrent imperative language, September 25, 2007. A preliminary version (without proofs, recursion and region-scoping) appeared in the proceedings of CONCUR'07, LNCS 4703 (2007), 272-286.
[Abstract, pdf, slides (pdf)]

Reactive concurrent programming revisited,with R. Amadio, F. Boussinot and I. Castellani, ENTCS Vol. 162 (2006) 49-60
[Abstract, pdf]

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 Vol. 114 (1993), 31-61.
[Abstract]

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

The chemical abstract machine, with G. Berry, in Theoretical Computer Science 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 Fundamenta Informaticae XI (1988), 433-453.
[Abstract]

Concurrency and atomicity, with I. Castellani, in Theoretical Computer Science 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 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 Vol. 22 (1983), 135-173.
[Abstract]