Linear Logic by Asymmetric Levels, Memoire for the Master's degree, under the supervision of
Damiano Mazza (
pdf).
Abstract: We introduce a fragment of Linear Logic through restrictions on it's graphical representation: proof nets. We then show all representable functions in this fragment are polynomially bounded.
Introduction to pi-calculus, talk during the
Vérité et Preuve day of nevembre 2010 (
beamer).
Abstract: Simple introdution to techniques of pi-calculus for philosophers: intentions, formalization, bisimilarity, asynchrony.
Interaction Solos, talk during the Final Meeting of the
ChoCo Project (
beamer)
and a meeting of the
Panda project (
beamer).
Abstract: We build a language of processes corresponding exactly to the most general Interaction Nets in which cells "are" solos. We then introduce an unusual subcalculus and show it is as expressive as the whole system: names are shared by at most two processes. In other words, channels only connects two processes (a bit like a physical wire can only connect two machines). This first result leads us to a possible classification of complexity of non-determinism.
Structural Operational Semantics for Graph Rewriting presented at the
ICE workshop 2011 (
pdf,
arxiv).
Abstract:
Process calculi and graph transformation systems provide models of reactive systems with labelled transition semantics. While the semantics for process calculi is compositional, this is not the case for graph transformation systems, in general. Hence, the goal of this article is to obtain a compositional semantics for graph transformation system in analogy to the structural operational semantics (SOS) for Milner’s Calculus of Communicating Systems (CCS).
The paper introduces an SOS style axiomatization of the standard labelled transition semantics for graph transformation systems. The first result is its equivalence with the so-called Borrowed Context technique. Unfortunately, the axiomatization is not compositional in the expected manner as no rule captures “internal” communication of sub-systems. The main result states that such a rule is derivable if the given graph transformation system enjoys a certain property, which we call “complementarity of actions”. Archetypal examples of such systems are interaction nets. We also discuss problems that arise if “complementarity of actions” is violated.