Maxime Gamboni

Research | [Curriculum Vitæ] | [Software] | [Novels & Short Stories] | [Zen Code]

Contact

Myself

I was born in Switzerland in 1981 and graduated in 2004 at the EPFL (Swiss Federal Institute of Technology) in Computer Science.

I got my PhD in Mathematics at IST in December 2010, under the supervision of António Ravara.

I also am a student member of the Security and Quantum Information Group.

My current research interests are Behavioural Type Systems for Process Calculi

Papers

Responsive Choice in Mobile Processes (In Proceedings of the TGC 2010 Conference) [pdf] [ps.gz] [bib] [slides]

We propose a general type notation, formal semantics and a sound, compositional, and decidable type system to characterise some liveness properties of distributed systems.

In the context of mobile processes, we define two concepts, activeness (ability to send/receive on a channel) and responsiveness (ability to reliably conduct a conversation on a channel), that make the above properties precise.

The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process.

Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or conversations (where the protocol may permit more than one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns.

Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.

First published on 24 February 2010. Presented at TU Berlin on 15 March 2010. Presented at IST, Lisbon on 14 May 2010. Presented at FCT, Monte de Caparica on 19 May 2010.

Activeness and Responsiveness in Mobile Processes (In Proceedings of the ConfTele 2009 Conference) [pdf] [ps.gz] [bib] [slides]

In mobile processes, a channel can be active (able of sending/receiving) or responsive (provide a reply to, or parameters for, a request), or both. It has a multiplicity such as ω (usable arbitrarily many times) or plain (unrestricted behaviour).

The context the process will be running in is similarly described, specifying to what extent third-party processes may interfere.

We outline semantic definitions of the properties, and a sound, compositional, type system enjoying subject-reduction, which verifies that, in a given process, channels behave as specified, and indicates, when applicable, what should be provided to the process before the properties hold.

Last updated on 27 April 2009. First published on 5 May 2009. Presented at TU Berlin on 26 May 2009.

Presentations

Behavioural Type Systems: Algorithms Analysing Algorithms: [slides]

A "behavioural type system" is an algorithm that discovers "behavioural properties" of programs by analysing their source code. Examples are determinacy, lack of side effects, risks of entering infinite loops or guarantees that all requests eventually get answered. In my talk I will give concrete examples of behavioural properties, explain what is a type system. I will describe a small "programming language" (the pi-calculus) and show how a type system working with "dependency analysis" can find behavioural properties in it. Finally I will say a word on the "generic type system" I designed during my PhD to capture the essence of dependency analysis.

Presented at GITAM University, Visakhapatnam on 5 December 2011.

Dependency Analysis: [slides]

I will present a generic type system characterising two broad classes of pi-calculus properties ("existential" and "universal" properties). The type system uses dependency analysis to compose dependency statements produced by user-provided elementary rules into complex behavioural statements that describe the whole process. Types describe a process as an open system and are able to predict how the process behaviour will evolve when other components are added to it. Types form a Boolean algebra that naturally integrates choice and branching.

Presented at WSBT'11, Monte de Caparica on 20 April 2011.

Responsive Choice in Mobile Processes (Short Presentation at the LICS 2009 Conference) [pdf] [bib] [cost slides] [lics slides]

In this short presentation we outline our current research on integrating choice and responsiveness, which permits statically guaranteeing responsiveness on process constructs that are necessary for encoding data, but that could not be analysed by existing works. Moreover, conditional properties permit analysing components of a system individually. We are developing a general type notation, formal semantics and a sound type system which are able to recognise most common kinds of data encodings such as Booleans, numbers, lists, and so on, as well as any non-recursive function on them.

Presented at Sensoria, Lisbon on 9 June 2009. Presented at COST Action, Lisbon on 12 June 2009. Presented at LICS'09, Los Angeles on 12 August 2009.

Type Checking Liveness Properties of Mobile Processes: [slides]

This presentation is about a number of type systems and algorithms designed to guarantee a number of desirable properties for a typical client-server interaction.

In particular, we want the server to be ready to handle arbitrarily many requests and at any time, all requests should eventually get answered, the processing of a request should eventually terminate, and given a protocol governing negotiation of resources between the client and the server, both parties should obey to it.

Having given and informal description of these properties as well as the language being used (the pi-calculus), I will describe and compare a number of type systems enforcing these properties in processes:

I will start by describing and demonstrating an existing implementation of a type system written by Naoki Kobayashi, "TyPiCal".

Secondly, I will describe the work António Ravara and I have been doing on the topic.

Finally, I will cover a number of other type systems (Deng and Sangiorgi's type system for termination, and Kobayashi and Sangiorgi's lock-freedom analysis), comparing their expressive power.

Presented at University of Glasgow on 3 April 2008. Presented at EPFL on 7 May 2008. Last updated on 30 October 2008.

What is TyCO, after all ? (Final presentation of my diploma work) [slides]

Presented at EPFL on 15 March 2004. Presented at FCUL on 30 June 2004.

What is TyCO, after all ? (Final presentation of my diploma work) [slides]

Presented at IITM on 23 February 2004.

What is TyCO, after all ? (Intermediary presentation of my diploma work) [slides]

Presented at IITM on 27 November 2003.

Technical Reports

These are unpublished works in progress:

Responsive Choice in Mobile Processes: [pdf]

We propose a general type notation, formal semantics and a sound, compositional, and decidable type system that characterise some liveness properties of distributed systems supporting choice. When such systems are specified using mobile processes, it is important to provide a number of liveness guarantees, such as, from a client's point of view, ``If I send a request, will it eventually be received? Will it eventually be processed, and will I eventually obtain an answer?'', or, from a server's point of view, ``Will I eventually receive a request? Will my clients respect the protocol?''.

We define two concepts, activeness (ability of sending/receiving on a channel) and responsiveness (ability to reliably conduct a conversation), that make the above properties precise, in particular what ``eventually'' and ``respect the protocol'' mean. The semantic definitions are respected by the type system, in the sense that the logical statements it outputs are correct descriptions of the process, according to the semantics.

In process calculi, processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or of object-oriented style programming (where a call matches one method out of a set). Our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns.

Finally, compositionality features are offered through the use of conditional properties that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.

Last updated on 24 February 2012.

Activeness and Responsiveness: [pdf]

In this paper we propose a new way of writing channel and process types for the π-calculus, as well as a semantic description of two liveness properties of channels: activeness (whether the process is able to receive or send a request on the channel) and responsiveness (if a receiver is able to eventually reply to a request).

Any combination of these properties can be associated independently to input and output occurrences of names in a process and to their parameters (thus specifying what a name polar may expect from its complement).

The type notation we propose puts an emphasis on protocols: A channel type segregates the server (input) side behaviour from the client (output) behaviour, and the type for a process explicitly specifies how third-party processes are permitted to interact and interfere with it.

We conclude the paper with a survey of some works on related topics along with encodings of the various type notations.

Last updated on 30 January 2009.

Deciding Deterministic Responsiveness and Closeness in π-calculus: [pdf] [ps.gz] [bib] [slides]

In order to write encodings of complex data structures in π-calculus we need guarantees that certain fundamental properties of communication are preserved when interacting with encoded processes. These include non-interference of the data transmission subprocess, responsiveness for data decoding requests, unicity of the transmitted value and immutability of a transmitted value. We propose a type system of π-calculus processes for which any typable process satisfies the above requirements.

Presented at FCUL on 28 June 2006. Last updated on 21 September 2006.

Theses

Statically Proving Behavioural Properties in the π-calculus via Dependency Analysis (My PhD Thesis) [pdf] [slides]

In this thesis I present a generic semantic framework and sound type system suited for analysing a wide variety of behavioural properties in π-calculus processes, both liveness properties such as activeness (a generalisation of receptiveness), termination and reachability, and safety properties such as determinism and isolation.

Dependency analysis is a central ingredient of this framework, implemented by dependency statements describing process properties conditional on some resources to be provided by third-party processes. Dependency statements are used as elementary ingredients of behavioural statements, logical statements that precisely characterise negotiation of resources between a process and its environment. Dependency analysis provides this framework with powerful compositionality: when arranging pre-analysed (typed) components together, the resulting process' type can be directly derived from those of the components, with no need to re-analyse the entire process. Behavioural statements also integrate primitives for describing selection (choices made by a process) and branching (choices offered by a process).

The type system, parametrised with elementary rules giving the essence of the desired properties and channel types giving communication protocols to be used on communication channels, automatically constructs a behavioural statement by automatically analysing processes.

First published on 1 August 2010. Presented at IST, Lisbon on 17 December 2010. Last updated on 26 December 2010.

What is TyCO? (My Diploma — Master — Thesis) [pdf] [ps.gz] [bib]

We study the expressive power of asynchronous π-calculus with nested variants (πav) and of TyCO by means of encodings.

TyCO can be seen as a sub-calculus of πav, in that TyCO only allows one level of variants, the only difference being that πav requires a separate construct for analysing an input while in TyCO input and value analysis are tightly bound. Still, we can give an encoding (embedding) that is fully abstract and good.

We propose a fully abstract encoding from πav to TyCO.

Errata

There is a crucial hole in the operational correspondence proposition, that triggered our research on determinism, closeness and activeness. Consider the πav process

P = case t of {...}

where t is a name. This process does not reduce because t is not a composite value (the process can be simply typed if t has a variant type). However its encoding is

[[P]]=(νu)(u»t | u!d(r)...)

which has the transitions [[P]]   τ  t!d(r')→ ... This contradicts the operational correspondence Proposition (5.2.3.6.c). That structural congruence statement on the very top of page 59 (just before section B.14) is wrong. This cascades to full abstraction (page 60, top) that assumes any decoding query is answered internally in the process and not sent to the environment.

If we reject P as being malformed, saying any case statement must either have structured values or be on a (non-free) input parameter variable, then let instead P0=a(t).P. Then the transition P0   a(t)P must be ruled out as invalid because it generates a malformed process. Yet this is precisely what the proof of the full abstraction theorem does when handling input transitions: Point 2 on page 59 "Taking v=t (...) we meet the requirements of receptive bisimulation".

In general, Sangiorgi's trick of "trigger names" works fine for receptiveness, but not for properties we require in this encoding, such as lack of side effects, determinism, etc, because any such guarantees are invalidated once we do a forward from a "discreet" name to a plain name.

First published on 25 March 2004. Last updated on 20 April 2009.

(This space intentionally left blank)