Cosimo Laneve

I&C Journal 2017 Journal Article

Deadlock analysis of unbounded process networks

• Naoki Kobayashi
• Cosimo Laneve

Deadlock detection in concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale. To enable the analysis of such programs, (1) we define an algorithm for detecting deadlocks of a basic model featuring recursion and fresh name generation: the lam programs, and (2) we design a type system for value-passing CCS that returns lam programs. We show the soundness of the type system, and develop a type inference algorithm for it. The resulting algorithm is able to check deadlock-freedom of programs that cannot be handled by previous analyses, such as those that build unbounded networks.

LOPSTR Conference 2017 Conference Paper

Deadlock Detection of Java Bytecode

• Cosimo Laneve
• Abel Garcia

Abstract This paper presents a technique for deadlock detection of Java programs. The technique uses typing rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language – the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.

TCS Journal 2008 Journal Article

A simple calculus for proteins and cells

• Cosimo Laneve
• Fabien Tarissan

The use of process calculi to represent biological systems has led to the design of different formalisms such as brane calculi and κ -calculus. Both have proved to be useful to model different types of biological systems. As an attempt to unify the formalisms, we introduce the bio κ -calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. In bio κ -calculus, protein–protein interactions have to be at most binary and cell interactions have to fit with sort constraints. In this contribution we define the semantics of bio κ -calculus, analyse its properties, discuss the expressivity of the calculus by modelling two significant examples–a signalling pathway and a virus infection–and study an implementation in Milner’s π -calculus.

I&C Journal 2007 Journal Article

Linear forwarders

• Philippa Gardner
• Cosimo Laneve
• Lucian Wischik

A linear forwarder is a process that receives one message on a channel and sends it on a different channel. We use linear forwarders to provide a distributed implementation of Milner’s asynchronous pi calculus. Such a distributed implementation is known to be difficult due to input capability, where a received name is used as the subject of a subsequent input. This allows the dynamic creation of large input processes in the wrong place, thus requiring comparatively large code migrations in order to avoid consensus problems. Linear forwarders constitute a small atom of input capability that is easy to move. We show that the full input capability can be simply encoded using linear forwarders. We also design a distributed machine, demonstrating the ease with which we can implement the pi calculus using linear forwarders. We also show that linear forwarders allow for a simple encoding of distributed choice and have “clean” behaviour in the presence of failures.

TCS Journal 2004 Journal Article

Formal molecular biology

• Vincent Danos
• Cosimo Laneve

A language of formal proteins, the κ-calculus, is introduced. Interactions are modeled at the domain level, bonds are represented by means of shared names, and reactions are required to satisfy a causality requirement of monotonicity. An example of a simplified signalling pathway is introduced to illustrate how standard biological events can be expressed in our protein language. A more comprehensive example, the lactose operon, is also developed, bringing some confidence in the formalism considered as a modeling language. Then a finer-grained concurrent model, the mκ-calculus, is considered, where interactions have to be at most binary. We show how to embed the coarser-grained language in the latter, a property which we call self-assembly. Finally we show how the finer-grained language can itself be encoded in π-calculus, a standard foundational language for concurrency theory.

TCS Journal 2003 Journal Article

A type system for JVM threads

• Cosimo Laneve

The current definition of the Java bytecode verifier, as well as the proposals to formalize it, does not include any check about the structured use of locks by monitorenter and monitorexit instructions. So code is run, even if critical sections are corrupted. In this paper, we isolate a sublanguage of the Java Virtual Machine with thread creation and mutual exclusion. For this subset, we define a semantics and a formal verifier that enforces basic properties of threads and lock and unlock operations. The verifier integrates well with previous formalizations of the Java bytecode verifier. Our analysis of structured use of locks reveals the presence of bugs in the current compilers from Sun, IBM and Microsoft.

TCS Journal 2001 Journal Article

Bisimulations in the join-calculus

• Cédric Fournet
• Cosimo Laneve

We develop a theory of bisimulations in the join-calculus. We introduce a refined operational model that makes interactions with the environment explicit, and discuss the impact of the lexical scope discipline of the join-calculus on its extensional semantics. We propose several formulations of bisimulation and establish that all formulations yield the same equivalence. We prove that this equivalence is finer than barbed congruence, but that both relations coincide in the presence of name matching.

TCS Journal 1996 Journal Article

Interaction systems II: The practice of optimal reductions

• Andrea Asperti
• Cosimo Laneve

Lamping's optimal graph reduction technique for the λ-calculus is generalized to a new class of higher-order rewriting systems, called Interaction Systems. Interaction Systems provide a nice integration of the functional paradigm with a rich class of data structures (all inductive types), and some basic control flow constructs such as conditionals and (primitive or general) recursion. We describe a uniform and optimal implementation, in Lamping's style, for all these features. The paper is the natural continuation of [3], where we focused on the theoretical aspects of optimal reductions in Interaction Systems (family relation, labeling, extraction).

I&C Journal 1996 Journal Article

The Discriminating Power of Multiplicities in theλ-Calculus

• Gérard Boudol
• Cosimo Laneve

Theλ-calculus with multiplicities is a refinement of the lazyλ-calculus where the argument in an application comes with a multiplicity, which is an upper bound to the number of its uses. This introduces potential deadlocks in the evaluation. We study the discriminating power of this calculus over the usualλ-terms. We prove in particular that the observational equivalence induced by contexts with multiplicities coincides with the equality of Lévy–Longo trees associated withλ-terms. This is a consequence of the characterization we give of the corresponding observational precongruence, as an intensional preorder involvingη-expansion, namely, Ong's lazy Plotkin–Scott–Engeler preorder.

TCS Journal 1995 Journal Article

Paths, computations and labels in the λ-calculus

• Andrea Asperti
• Cosimo Laneve

We provide a new characterization of Lévy's redex-families in the λ-calculus (Lévy, 1978) as suitable paths in the initial term of the derivation. The idea is that redexes in a same family are created by “contraction” (via β-reduction) of a unique common path in the initial term. This fact gives new evidence about the “common nature” of redexes in a same family, and about the possibility of sharing their reduction. In general, paths seem to provide a very friendly and intuitive tool for reasoning about redex-families, as well in theory (using paths, we shall provide a remarkably simple proof of the equivalence between extraction (Lévy, 1978) and labeling) as in practice (our characterization underlies all recent works on optimal graph reduction techniques for the λ-calculus (Lamping, 1990; Gonthier et al. , 1992, Asperti, to appear), providing an original and intuitive understanding of optimal implementations). Finally, as an easy by-product of the path-characterization, we prove that neither overlining nor underlining are required in Lévy's labeling.

MFCS Conference 1992 Conference Paper

Mobility in the CC-Paradigm

• Cosimo Laneve
• Ugo Montanari

MFCS Conference 1991 Conference Paper

The Limit of Split_n-Bisimulations for CCS Agents

• Roberto Gorrieri
• Cosimo Laneve