Gruppo di Logica e Geometria della Cognizione

Proof nets for multiplicative linear logic (MLL) provide canonical representations of proofs: they are permutation-independent, separable and are injectively interpreted in the relational and coherent semantics. None of these properties scales to second order multiplicative linear logic (MLL2): proof nets for MLL2 are not invariant with respect to all valid permutations, are not separable and are not injectively interpreted in either the relational or coherent semantics. This problem is related to the interpretation of the existential quantifier. In categorical terms this should correspond to a coend, whereas the usual proof net representation violates the diagrams defining a coend. Starting from this intuition, we investigate the problem of defining canonical proof nets for MLL2 as a coherence problem for coends over a compact-closed category and we show some results concerning some fragments of MLL2.

La teoria della realizzabilità classica è stata introdotta da J.-L. Krivine negli anni 2000 a seguito di una intuizione di T. Griffin, che ha tipato l'istruzione "callcc" in Scheme (simile alla istruzione "try-catch" in Java) con la regola dell'assurdo (nella forma di legge di Pierce). Questo ha portato a generalizzare la corrispondenza di Curry-Howard a tutta la logica classica, ed anche oltre: assiomatizzando la nozione di programma (lambda-termine) e di esecuzione (programma + pila di esecuzione), grazie alle "algebre di realizzabilità", si riesce ad associare programmi a dimostrazioni (classiche) che usino assiomi supplementari - come ad esempio quelli della teoria degli insiemi. Questi programmi, chiamati "realizzatori" della formula dimostrata, ne forniscono una "giustificazione" che è una semantica intermedia tra quella Tarskiana (vero/falso) e quella data dalle dimostrazioni. In questo incontro ci concentreremo sull'assioma dell'ultrafiltro ("esiste un ultrafiltro non triviale sull'algebra di Boole delle parti di N") nel quadro della aritmetica al secondo ordine.

We show that the normal form of the Taylor expansion of a lambda-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier’s original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad-hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a non-deterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier’s approach can be preserved in this setting.

Software systems may leak information about confidential data.
Information theory helps in mathematically analyze and automatically quantify such leaks.

However, there is an (uncountable) infinity of leakage measures.
Hence a question arises: can we design countermeasures to information leakage
that are universally optimal, i.e. that guarantee minimal leakage no matter
which leakage measure is chosen?

We show contexts when this can be achieved, a counterexample to a general
solution and discuss potential applications of these techniques to security and privacy problems.

(This is a joint work with Arman Khouzani)

In Frege and Russell’s line, the main tool to propagate ontology toward higher orders is realized by quotienting sets by equivalence relations. Indeed, this leads to produce, at the next order, separated individualities (disjoint non empty subsets covering the original set) and this in such a way that this separation is conceptually generated from a relation at the initial order.
This way to relate ontology and equivalence relations is deeply Parmenidian in inspiration : non only because it considers individualities independently of time (first point), but also because it propagates at the next order the idea of an autonomy of individualities, i.e. the idea that the individuality of individuals is independent of any relational commitment between them (second point).
"Denotational semantics of programs" (the research programme launched by Strachey and Scott around 1969) can be seen as a first step to substitute to Parmenidian ontology an Heraclitean ontology, in the sense that it faces the first point (individualities in time): in a computational universe, transformation comes first and separation phenomenas are generated by (and compatible with) these transformation.
In that talk, I will present my current work on a complementary program toward a non Parmenidian ontological point of view facing the second point (Agonal ontology) which starts by introducing a generalization of equivalence relations, collusions (total and surjective collusive relations). After having presented their main properties, notably with respect to the partitioning purpose, I will conclude about logical potential interpretations.

In questo incontro studieremo come le combinatorial proofs di Hughes possono essere utilizzate per definire una nozione di equivalenza tra dimostrazioni per la logica classica. Mostreremo poi come diversi formalismi (calcolo dei sequenti, alberi di refutazione e resolution) possano essere tradotti in combinatorial proofs e quale nozione di identità viene definita da ciascuno di essi.

We shall be interested in the asymptotic dynamical properties of Boolean networks: fixed points, attractive cycles, and more general attractors. While the properties of Boolean networks without local cycle or without local positive cycle are rather well understood, recent literature raises the following two questions about networks without local negative cycle. Do they have at least one fixed point? Should all their attractors be fixed points? We give negative answers to both questions: we show that and-nets without local negative cycle may have no fixed point, and that Boolean networks without local negative cycle may have (antipodal) attractive cycles.

The emergence of the concepts of cellular automata (CA) (Wolfram, 1983, 1984, 1986) and Boolean (BN) network (Kauffman, 1969), between the end of the 60s and early 80s, for the formalization of computational processes and genetic regulation, respectively, was a first step in the development of modeling of evolutionary phenomena using networks. This type of modeling has been useful to solve various problems in other Sciences such as Chemistry (see Kier & Seybold, 2009; Kier, Seybold & Cheng 2005; Scalise & Schulman, 2015), Physics (see Chopard & Droz, 1998), Biology (see Deutsch & Dormann, 2004, Toroczkai & Güçlü, 2007), Ecology (see Dieckman, Law & Metz, 2000; Hofbauer & Sigmund, 2003; Hogeweg, 1988), even of Social Sciences like Psychology or Sociology (see Abraham, 2015; Kempe, Kleminberg & Tardos, 2005).
This new paradigm of modeling has evolved in recent years, giving rise to the concept of graph dynamical system (GDS), which generalizes the previous ones, since it contemplates that the relationships among elements of the system can be arbitrary. That is, the graph representing the relations among elements of the system, called dependency graph, could be arbitrary. In this generalization, the smallest units of aggregation of the phenomenon are called nodes (or vertices), in relation to their membership in the graph, relieving the term of cells in a CA and entities in a BN.
In this talk, we discuss some of the advances in the study of the periodic structure of a GDS when the evolution operator is a maxterm or minterm Boolean function.

Starting from works aimed at extending the Curry-Howard correspondence to process calculi through linear logic, we give another Curry-Howard counterpart for Milner's Calculus of Communicating Systems (CCS) by taking Ludics as the target system. Indeed interaction, Ludics' dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. CCS processes are interpreted into carefully defined behaviours of Ludics using a new construction, called directed behaviour, that allows controlled interaction paths by using pruned designs. Execution of processes is characterized as interaction on behaviours, by implicitly representing the causal order and conflict relation of event structures. As a direct consequence, we are also able to interpret deadlocked processes, and identify deadlock-free ones.