Author name cluster

Vincent Danos

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers

2 author rows

I&C Journal 2011 Journal Article

Probabilistic coherence spaces as a model of higher-order probabilistic computation

Vincent Danos
Thomas Ehrhard

We study a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the functional language PCF. We give a probabilistic interpretation of the semantics of probabilistic PCF closed terms of ground type. Last we suggest a generalization of this approach, using Banach spaces.

Details DOI

TCS Journal 2009 Journal Article

How liquid is biological signalling?

Vincent Danos
Linus J. Schumacher

This paper proposes an investigation of the global statistics of synthetic protein networks—a step towards a systemic understanding of their design space. We derive a liquidity index which describes the onset of the phase transition where an ensemble of agents aggregates into a giant cluster. This index captures the influence of both the domain distribution of agents and the binding strengths of their various domains in the limit of infinite populations. In simple cases it is possible to derive an explicit analytical expression of this index, which allows one to compare with simulations, and get a sense of how it transfers to the concrete finite case.

Details DOI

TCS Journal 2008 Journal Article

Computational self-assembly

Pierre-Louis Curien
Vincent Danos
Jean Krivine
Min Zhang

The object of this paper is to probe the computational limits of an applied concurrent language called κ. This language describes how agents can bind and modify each other. It is meant as a syntactic medium to build, discuss and execute descriptions of cellular signalling pathways. However, it can be studied independently of its intended interpretation, and this is what we are doing here. Specifically, we define a reduction of κ to a fragment where interactions can involve at most two agents at a time. The translation relies on an implicit causality analysis which permits escaping deadlocks. It incurs only a linear blow up in the number of rules. Its correctness is spelt out in terms of the existence of a specific weak bisimulation and is proved in detail. To compensate for the binary restriction, one allows components to create unique names. When using acyclic rules, this additional facility of name creation is not needed and κ can be reduced to a binary form as is.

Details DOI

I&C Journal 2006 Journal Article

Bisimulation and cocongruence for probabilistic systems

Vincent Danos
Josée Desharnais
François Laviolette
Prakash Panangaden

We introduce a new notion of bisimulation, called event bisimulation on labelled Markov processes (LMPs) and compare it with the, now standard, notion of probabilistic bisimulation, originally due to Larsen and Skou. Event bisimulation uses a sub σ-algebra as the basic carrier of information rather than an equivalence relation. The resulting notion is thus based on measurable subsets rather than on points: hence the name. Event bisimulation applies smoothly for general measure spaces; bisimulation, on the other hand, is known only to work satisfactorily for analytic spaces. We prove the logical characterization theorem for event bisimulation without having to invoke any of the subtle aspects of analytic spaces that feature prominently in the corresponding proof for ordinary bisimulation. These complexities only arise when we show that on analytic spaces the two concepts coincide. We show that the concept of event bisimulation arises naturally from taking the co-congruence point of view for probabilistic systems. We show that the theory can be given a pleasing categorical treatment in line with general coalgebraic principles. As an easy application of these ideas we develop a notion of “almost sure” bisimulation; the theory comes almost “for free” once we modify Giry’s monad appropriately.

Details DOI

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.

Details DOI

TCS Journal 2004 Journal Article

Modeling and querying biomolecular interaction networks

Nathalie Chabrier-Rivier
Marc Chiaverini
Vincent Danos
François Fages
Vincent Schächter

We introduce a formalism to represent and analyze protein–protein and protein–DNA interaction networks. We illustrate the expressivity of this language, by proposing a formal counterpart of Kohn's compilation on the mammalian cell-cycle control. This effectively turns an otherwise static knowledge into a discrete transition system incorporating a qualitative description of the dynamics. We then propose to use the computation tree logic (CTL) as a query language for querying the possible behaviors of the system. We provide examples of biologically relevant queries expressed in CTL about the mammalian cell-cycle control and show the effectiveness of symbolic model checking tools to evaluate CTL queries in this context.

Details DOI

TCS Journal 2003 Journal Article

Computational isomorphisms in classical logic

Vincent Danos
Jean-Baptiste Joinet
Harold Schellinx

All standard ‘linear’ boolean equations are shown to be computationally realized within a suitable classical sequent calculus LK p η. Specifically, LK p η can be equipped with a cut-elimination compatible equivalence on derivations based upon reversibility properties of logical rules. So that any pair of derivations, without structural rules, of F⇒G and G⇒F, where F, G are first-order formulas ‘without any qualities’, defines a computational isomorphism.

Details DOI

I&C Journal 2003 Journal Article

Linear logic and elementary time

Vincent Danos
Jean-Baptiste Joinet

A subsystem of linear logic, elementary linear logic, is defined and shown to represent exactly elementary recursive functions. Its choicest part consists in reducing the deductive power of the exponential, also known as the “bang, ” which, in linear logic, is in charge of controlling duplication in the cut-elimination process.

Details DOI

CSL Conference 2001 Conference Paper

The Anatomy of Innocence

Vincent Danos
Russell Harmer

Abstract We reveal a symmetric structure in the ho/n games model of innocent strategies, introducing rigid strategies, a concept dual to bracketed strategies. We prove a direct definability theorem of general innocent strategies with respect to a simply typed language of extended Böhm trees, which gives an operational meaning to rigidity in call-by-name. A corresponding factorization of innocent strategies into rigid ones with some form of conditional as an oracle is constructed.

Details

CSL Conference 2000 Conference Paper

Disjunctive Tautologies as Synchronisation Schemes

Vincent Danos
Jean-Louis Krivine

Abstract In the ambient logic of classical second order propositional calculus, we solve the specification problem for a family of excluded middle like tautologies. These are shown to be realized by sequential simulations of specific communication schemes for which they provide a safe typing mechanism.

Details

TCS Journal 1999 Journal Article

Reversible, irreversible and optimal λ-machines

Vincent Danos
Laurent Regnier

Lambda-calculus is the core of functional programming, and many different ways to evaluate lambda-terms have been considered. One of the nicest, from the theoretical point of view, is head linear reduction. We compare two ways of implementing that specific evaluation strategy: “Krivine's abstract machine” and the “interaction abstract machine”. Runs on those machines stand in a relation which can be accurately described using the call/return symmetry discovered by Asperti and Laneve.

Details DOI

CSL Conference 1998 Conference Paper

Timeless Games

Patrick Baillot
Vincent Danos
Thomas Ehrhard
Laurent Regnier

Abstract Two models of classical linear logic are set up. First our recent version of AJM games model which will be our source model. Then the target model, polarized pointed relations, a variant of the plain relational model which is constructed in two steps: first the model of pointed relations, then the additional polarization structure which yields a proper duality. Then the natural time-forgetting map is shown to generate a lax functor from the source to the target. Finally a further refinement of the target model using bipolarities is sketched, giving a closer link with the games model for the interpretation of syntax. Thus a bridge is constructed that goes from a dynamic model to a static model of evaluation.

Details

CSL Conference 1997 Conference Paper

Directed Virtual Reductions

Vincent Danos
Marco Pedicini
Laurent Regnier

Abstract This note defines a new graphical local calculus, directed virtual reductions. It is designed to compute Girard's execution formula EX, an invariant of closed functional evaluation obtained from the “geometry of interaction” interpretation of λ-calculus [5]. The calculus is obtained by synchronizing another graphical local calculus presented in “local and asynchronous beta-reduction”: virtual reductions [4]. This synchronization makes it easier to mechanize than general virtual reductions. In undirected virtual reductions the consistency of the computation is insured by an algebraic mechanism called the bar. This mechanism in general induces correction terms of any order. The directed virtual reduction has been designed to keep those terms at order one. A further synchronization, the combustion strategy will even wipe out first order correction terms. Applied to sharing graphs, the combustion strategy yields Lamping's optimal graphical calculus as presented in [1]. But more efficient optimal implementations of λ-calculus are expected. The paper is conceived as a follow-up of [4] and supposes a familiarity with virtual reduction.

Details