Gruppo di Logica e Geometria della Cognizione

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.

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).

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.

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.

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.

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 » 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.

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.

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.