Linear Logic by Asymmetric Levels
, Memoire for the Master's degree, under the supervision of Damiano Mazza
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.
, talk during the Final Meeting of the ChoCo Project
and a meeting of the Panda project
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
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 ﬁrst 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.