Gérard Boudol

Welcome to my home page. I am an Emeritus Researcher at INRIA, Sophia-Antipolis Méditérranée, within the INDES project. My research interests include theory of concurrency (process algebras, verification, ``true concurrency'', multithreading, relaxed memory models), 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.

This picture was taken in 1998. Another, more recent side of me is here

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) -- now CiteSeerX, 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: security, mobility (especially pi-calculus and its variants), lambda-calculus, concurrency and verification, semantics of objects, term rewriting systems.

Secure information flow as a safety property, March 2008. A short version (without proofs) appears in the proceedings of FAST'08, LNCS 5491 (2009) 20-34.
[Abstract, .pdf, slides]

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

On declassification and the non-disclosure policy, with A. Almeida Matos, March 2007. Published in the J. of Computer Security Vol. 17 No. 5 (2009) 549-597.
[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: 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.

Typing safe deallocation, ESOP'08, LNCS 4960 (2008) 116-130.
[Abstract, pdf]

On strong normalization and type inference in the intersection type discipline, in "Calculi, Types and Applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca" (S. Berardi and U. de Liguoro, Eds), Theoretical Computer Science Vol. 398 No. 1-3 (2008) 63-81.
[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 ]

Relaxed semantics of concurrent programming languages, with G. Petri et B. Serpette, April 2012 (submitted).
[Abstract, pdf]

A theory of speculative computation, with G. Petri, December 2009. An extended abstract (without proofs) appeared in the proceedings of ESOP'10, LNCS 6012, 165-184.
[Abstract, pdf]

Typing termination in a higher-order concurrent imperative language. Information and Computation 208 (2010) 716-736, available online. A preliminary version (without recursion and proofs) appeared in the proceedings of CONCUR'07, LNCS 4703 (2007), 272-286.
[Abstract, pdf, slides (pdf)]

A deadlock-free semantics for shared memory concurrency, ICTAC'09, Lecture Notes in Computer Science 5684 (2009) 140-154.
[Abstract, pdf]

Relaxed memory models: an operational approach, with G. Petri, POPL'09.
[Abstract, pdf, slides]

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, pdf, 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, .pdf]

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

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]

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]