Gruppo di Logica e Geometria della Cognizione

We develop a methodology for studying and comparing the expressiveness of computational models which are based on rewriting. We consider a class of rewriting systems, which we call normal, admitting a natural interpretation in terms of event structures; this is done by building up on work of Mazurkiewicz, Nielsen, Plotkin, Winskel, Melliès, and Mimram. Then, we introduce the notion of bisimilar embedding of event structures, which allows us to say when a computational system is "at least as expressive" as another one, as soon as these two are described in terms of event structures. Finally, we prove a few separation results for normal rewriting systems based on this notion, and we give an application of these to interaction nets and their non-deterministic variants, including Ehrhard and Regnier's differential interaction nets.

La teoria antirealista del significato sviluppata a partire dagli anni '70 da Dummett, Prawitz e Martin-Löf, stabilisce diversi desiderata che le regole logiche devono soddisfare affinché esse possano caratterizzare adeguatamente i connettivi logici. In particolare, il requisito di armonia impone un "equilibrio deduttivo" che apparentemente non può essere soddisfatto che dalle regole della logica intuizionista.

Nella prima parte del talk, mostriamo in che senso l'isomorfismo di Curry-Howard rispecchia fedelmente tali condizioni richieste ad un calcolo logico. All'interno di questo quadro teorico, analizziamo alcuni limiti degli approcci tradizionali alla nozione di armonia e proponiamo un criterio sufficiente per definire un connettivo logico. Tale criterio rende conto del fatto che le proprietà dei connettivi intuizionisti hanno una natura fondamentalmente computazionale.

Nella seconda parte del talk, esaminiamo alcune possibili strategie per estendere alla logica classica il criterio proposto. Questo costituisce un primo passo verso la possibilità di valutare l´importanza filosofica della "costruttivizzazione" della logica classica.

In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints.

Starting from this result, in the present work we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: more precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (called cone defined by means of jumps. As consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can be partially overlapping. Moreover, we define normalization for exponential J-proof nets, proving, by Gandy's method, that even in case of ''superposed'' cones, reduction enjoys confluence and strong normalization.

Lo studio di sistemi dinamici adatti alla descrizione dei sistemi biologici e' sempre stato di fondamentale interesse per le implicazioni che puo' avere nelle applicazioni in medicina. La possibilita' di accedere a dati sperimentali che rendono la descrizione dei fenomeni biologici con un livello di dettaglio che si spinge fino al livello molecolare, rendono necessario l'utilizzo di modelli interpretativi della realta' in grado di spiegare fenomeni complessi.

Nello studio del sistema immunitario abbiamo proposto una nuova metodologia per combinare
- database di letteratura specialistica (dataminig),
- serie temporali di dati di microarray,
- modello della dinamica meno accurato,

e fornire un modello piu' accurato per la descrizione del sistema di interazione tra geni che governa la reazione del sistema immunitario (differenziazione delle cellule T).

Lavoro in preparazione: M. Pedicini, F. Barrenas, T. Clancy, F. Castiglione, E. Hovig, K. Kanduri, D. Santoni, M. Benson. Combining network modeling and gene expression microarray analysis to explore the dynamics of Th1 and Th2 cell regulation.

Roberto Avanzi (Bochum, Germany)
joint work with Clemens Heuberger (Graz, Austria)
and Helmut Prodinger (Stellenbosch, South Africa)

We consider digital expansions of scalars for supersingular Koblitz curves in characteristic three. These are expansions of integers to the algebraic base of TeX Embedding failed!, where TeX Embedding failed! is a zero of a polynomial TeX Embedding failed!. The obvious application of these expansions is to scalar multiplication on Koblitz curves.

A simple connection between TeX Embedding failed!-adic expansions and balanced ternary representations is given.

Windowed non-adjacent representations are considered whereby the digits are elements of minimal norm. We exploit the rotational symmetry of the digit set to reduce the memory requirements of scalar multiplication by a factor of six with respect to previous methods. Furthermore, we give an explicit description of the elements of the digit set, allowing for a very simple and efficient precomputation strategy.

Additionally, we explicitly describe the action of some endomorphisms on the Koblitz curve as a scalar multiplication by an explicitly given integer.