Gruppo di Logica e Geometria della Cognizione
coordinatore: V. Michele Abrusci


Dipartimento di Matematica e Fisica
Università Roma Tre
Largo San Leonardo Murialdo 1
00144 Roma -Italia


Il fondamento scientifico della costituzione del gruppo risiede nell'interesse che tutti i suoi componenti portano alla moderna teoria della dimostrazione. Questo settore della logica matematica ha conosciuto recentemente una vera e propria "rinascita", dovuta al suo incontro con l'informatica: la corrispondenza di Curry-Howard stabilisce una corrispondenza tra dimostrazioni e programmi e tra esecuzione dei programmi ed eliminazione del taglio (un procedimento di trasformazione delle dimostrazioni ben noto ai logici). La scoperta di questa semplice e fondamentale corrispondenza è il punto di partenza per un nuovo approccio alla nozione di costruttività in logica ed alla programmazione in informatica.

In quest'ambito si colloca l'apparizione della logica lineare, che unisce gli aspetti "costruttivi" della logica intuizionista alle simmetrie della logica classica. La logica lineare nasce da un'analisi matematica molto fine della semantica delle dimostrazioni della logica intuizionista. Dalla sua apparizione nel 1986, essa si è imposta come strumento usato in vari settori di ricerca, dalla teoria della dimostrazione al lambda-calcolo, dalle macchine astratte al calcolo distribuito, dalla teoria della complessità alla programmazione logica.


Open Call-by-Value (joint work with Beniamino Accattoli)

Giulio Guerrieri (Università Roma Tre - Université d'Aix-Marseille)
11/03/2016 - 11:00
Aula 311, Dipartimento di Matematica e Fisica, L.go San Leonardo Murialdo 1.

The elegant theory of the call-by-value lambda-calculus relies on
weak evaluation and closed terms, that are natural hypotheses in
the study of programming languages. To model proof assistants,
however, strong evaluation and open terms are required, and it is
well known that the operational semantics of call-by-value becomes
problematic in this case, as first pointed out by Paolini and Ronchi
della Rocca. Here we study the intermediate setting—that we call
Open Call-by-Value—of weak evaluation with open terms, on top
of which Grégoire and Leroy designed the abstract machine of Coq.
Various calculi for Open Call-by-Value already exist, coming from
logical, semantical, or implementative points of view, each one with
its pros and cons. This paper presents a detailed comparative study
of their operational semantics. First, we show that all calculi are
equivalent from a termination point of view, justifying the slogan
Open Call-by-Value. Second, we compare their equational theories.
Third, we present a detailed quantitative analysis of the time cost
model. Four, we introduce a new simple abstract machine, and
prove it a reasonable implementation of Open Call-by-Value with
respect to its cost model. Along the way, there emerges a sharp
deconstruction of call-by-value evaluation and of the complexity of
its implementations.

Diagrammi di corde per le reti di prova

Matteo Acclavio (Institut de Mathématiques de Marseille)
12/02/2016 - 11:00
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Aula 311

Le reti di prova in MELL necessitano di criteri di correttezza non locali o esterni alla sintassi delle reti di interazioni: connessione, aciclicita', box, salti.
Dopo aver introdotto la sintassi dei diagrammi di corde per le categorie monoidali, verra' descritto come ricostruire in questi contesti modelli di proof net con un unico criterio di correttezza locale per MLL e MELL (con o senza costanti).

New trends on linear logic proof-nets

Lorenzo Tortora de Falco (Dipartimento di Matematica e Fisica, Università Roma Tre)
Giulio Guerrieri (I2M, Université d'Aix-Marseille)
Università Roma Tre, Dipartimento di Matematica e Fisica (Largo San Leonardo Murialdo, 1 - 00146 Roma), Room 311 (3rd floor)


December 21, Monday

11:00-11:15 Ouverture
11:15-12:00 Daniel De Carvalho The relational model is injective for Multiplicative Exponential Linear Logic
12:00-12:30 Lorenzo Tortora de Falco/Luc Pellissier Some remarks about connectedness, Taylor expansion and injective relational semantics

12:30-14:00 lunch

14:00-14:45 Lionel Vaux Looking at cut elimination through the lens of Taylor expansion
14:45-15:15 Marco Solieri Taylor-expansion, cut elimination and geometry of interaction
15:15-16:00 Damiano Mazza Proof Nets in Space

16:00-16:15 coffee break

16:15-16:45 Ugo Dal Lago The Geometry of Synchronization
16:45-17:15 Anna Chiara Lai, Marco Pedicini, Silvia Rognone Quantum entanglement and the Bell Matrix: the encoding in QMLL

December 22, Tuesday

9:15-10:00 Marc Bagnol TBA

10:00-10:30 coffee break

10:30-12:30 open session Representation of nets
talks and micro-talks by Giulio Guerrieri/Lorenzo Tortora de Falco, Luc Pellissier, Thomas Ehrhard, Beniamino Accattoli, Vito Michele Abrusci.

12:30-14:30 lunch

14:30-17:00 open session Correctness criteria
talks and micro-talks by Roberto Maieli, Vito Michele Abrusci, Beniamino Accattoli, Marc Bagnol, Thomas Ehrhard.

Multi scale and multi omic approaches in systems medicine

Prof. Pietro Lio', Computer Laboratory, University of Cambridge, UK
18/12/2015 - 11:30
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre AULA 311 (SEMINARI) Largo San L. Murialdo,1

I will first introduce my current research on multi comics and multi scale modeling. Ductal carcinoma is one of the most common cancers among women, and the main cause of death is the formation of metastases. Through a branching process model, I describe the relation between the survival times
and the drivers mutations mainly involved in metastatic breast cancer. In particular, the model takes into account intracell to tissues dynamics in breast, blood and bone compartments and uses the gene expression profile of circulating tumour cells to predict personalised survival probability. I will end by introducing current work on logic approaches.

Algebraic Models for Systems Biology

Prof. Abdul Salam Jarrah
03/12/2015 - 11:00
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre AULA 311 (SEMINARI) Largo San L. Murialdo,1

Elucidating the topology and dynamics of biological networks from
experimental data is a central goal of systems biology. Recently
algebraic models have been introduced as a new framework for modeling
and analyzing biological networks as multi-states systems,
generalizing Boolean networks. Within this framework, using tools from
computational algebra and algebraic geometry, algorithmic methods that
find and present the model space have been developed, and the class of
nested canalyzing models have been characterized. Furthermore,
methods for analyzing the dynamics of monomial models have been
developed. The algebraic framework as well as some of the mentioned
methods will be presented in this talk.

Results and problems around a discrete dynamical system

Prof. Attila Pethö, University of Debrecen, Hungary
13/11/2015 - 11:30
Dipartimento di Matematica e Fisica Università degli Studi Roma Tre Aula 314, terzo piano, edificio C - Largo San Leonardo Murialdo,1

To the real vector TeX Embedding failed! we associate the mapping TeX Embedding failed! such that TeX Embedding failed!. This is the discrete dynamical system, which is the topic of our talk. It was introduced by S. Akiyama, H. Brunotte, T. Borb\'ely, J. Thuswaldner and called shift radix system, shortly SRS. The orbits of the iterations of TeX Embedding failed! can be divergent or periodic. In the later case they can be ultimately zero or not. The distinction of these cases leads to hard algorithmic and complexity question provided TeX Embedding failed! is a rational vector. We report on topological and geometric properties of regions associated to SRS.

Algorithmic and numerical solution of diophantine equations

Prof. Attila Pethö, University of Debrecen, Hungary
11/11/2015 - 16:00
Dipartimento di Matematica e Fisica Università degli Studi Roma Tre Aula F, primo piano, edificio Aule - Largo San Leonardo Murialdo,1

In our talk we give an overview on the development of the algorithmic and numerical theory of diophantine equations from Hilbert's problems until today. We focus our attention to the application of tools of transcendental and algebraic number theory as well as to diophantine approximation algorithms.

Proofs as schedules

Virgile Mogbil, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13
23/10/2015 - 11:00
Dipartimento di Matematica e Fisica, Università Roma Tre Largo S. Leonardo Murialdo 1, Roma Palazzina C, III piano, Aula 311

« Proofs as schedules » is a new approach about the proof-theoretic study of concurrent interaction. Through the Curry-Howard correspondence proof theory is well suited to describe confluent systems. Because the meaning of proofs lies in their normal forms, cut elimination should be confluent in order to preserve it. On the other hand concurrency has non-determinism as a fundamental feature. In process calculi the meaning of a term is not its final irreducible form but what happens to get there, as interaction with other processes... hence term reduction i.e. execution of interactions should definitely not preserve meaning. We propose a correspondence between proofs in linear logic and interaction plans for processes, called schedules.

Linear logic, polarization and evaluation strategies

Thomas Ehrhard CNRS, PPS - Universite' Paris Diderot - Paris 7
16/10/2015 - 11:00
Dipartimento di Matematica e Fisica, Univ. Roma Tre, Largo San Leonardo Murialdo, 1 edificio C, terzo piano, aula 311

There are two well known translations of the lambda-calculus into the multiplicative-exponential fragment of linear logic: the call-by-name and the call-by-value translations. The former is the standard "Girard's translation" and the latter was called "boring" by Girard in his seminal LL paper. We shall see how one can extend the lambda-calculus with simple constructions inspired by linear logic in order to factorize these translation through a single functional language admittedly much simpler than proof nets, and where weakening and contraction remain implicit. This calculus bears some similarities with Paul Levy's "call-by-push-value" and, just as the LL translation of classical systems, gives an essential role to the category of coalgebras of the exponential "!". It corresponds to a kind of half-polarized version of linear logic.

Colloquium di matematica: "On the mathematical interpretation of programs and proofs"

Thomas Ehrhard CNRS, directeur du laboratoire Preuves, Programmes et Syste'mes (PPS) Universite' Paris Diderot - Paris 7
evento esterno
14/10/2015 - 16:00
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre Aula F, primo piano, edificio Aule - Largo San Leonardo Murialdo,1

We shall see how the notions of monoidal categories, adjunctions and monads/comonads are deeply connected to the mathematical interpretation of functional computer programs and of mathematical proofs. We shall illustrate how this interpretation can suggest improvements of the syntax of programs. For instance, it allows to accommodate the call-by-name and the call-by-value evaluation strategies in a common functional setting, or provides a simple algebraic understanding of the "call with current continuation" primitive of the language scheme, both using the category of coalgebras of a comonad.