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

# News

## Quantum invariants for graph isomorphism

 Speaker: Fernando L. Pelayo Quando: 05/11/2021 - 15:00 Dove: Presso il Dipartimento di Matematica e Fisica in Largo San Leonardo Murialdo 1 - Edificio C - Aula 311 Online su Teams: https://bit.ly/3nQG8jM Abstract Venerdì 5 novembre 2021 alle ore 15:00, Fernando L. Pelayo (Castilla-La Mancha University - Department of Computer Science) Titolo: Quantum invariants for graph isomorphism Abstract: Since McKay presented his Nauty algorithm in 1981 to characterize graph isomorphism until the last proposal by Babai in 2015, a huge effort has been devoted to the graph isomorphism problem together with an improvement on their complexities. This problem is assumed to belong to neither P nor NP-Complete Computational Complexity classes. Maybe the most efficient deterministic algorithm on practice currently available is Traces algorithm proposed by McKay & Piperno in 2014. Quantum computing is facing this problem in an almost disruptive and very interesting perspective... Presso il Dipartimento di Matematica e Fisica in Largo San Leonardo Murialdo 1 - Edificio C - Aula 311 https://bit.ly/3nQG8jM L’annuncio è presente sul sito web dell’ateneo: https://www.uniroma3.it/articoli/quantum-invariants-for-graph-isomorphism-182302/

## Towards a denotational semantics for proofs in constructive modal logic

 Speaker: Davide CATTA Quando: 12/03/2021 - 15:00 Dove: Online su Teams http://bit.ly/30a9RZv Abstract Venerdì 12 marzo 2021 alle ore 15:00, si terrà il seminario del dott. Daniele Catta (Université di Montpellier) dal titolo "Toward a denotational semantics for proofs in constructive modal logic". Abstract Constructive modal logics are extensions of intuitionistic propositional logic with certain modal axioms. Many proof systems are known for these logics, but the only available denotational semantics is defined by means of an abstract construction, based on the quotient of their lambda terms. The general aim of our work is to define a game semantics for constructive modal logics. In this talk, I will define the winning strategies for a formula and show the correspondence between winning strategies and proofs. I will show how winning strategies can be defined as the projection of specific paths in a graphical proof system defined for this purpose - combinatorial proofs. (This talk is based on joint work with Matteo Acclavio and Lutz Straßburger) Per partecipare al seminario cliccare sul seguente Link http://bit.ly/30a9RZv

## Minimizing the Number of Unhappy Singles: Improved Approximation Algorithms for Stable Marriage

 Speaker: Chien-Chung Huang Quando: 05/03/2021 - 15:00 Dove: Online su teams https://bit.ly/3uPLhvf Abstract Venerdì 5 marzo 2021 alle ore 15:00, il dott. Chien-Chung Huang (CNRS / École Normale Supérieure PSL, Paris) presenterà il seminario di Logica e Informatica Teorica dal titolo: "Minimizing the Number of Unhappy Singles: Improved Approximation Algorithms for Stable Marriage". Abstract: We consider the problem of computing a large stable matching in a bipartite graph G = (A ? B, E) where each vertex u ? A ? B ranks its neighbors in an order of preference, perhaps involving ties. Let the matched partner of u in a matching M be M(u). A matching M is said to be stable if there is no edge (a,b) such that a is unmatched or prefers b to M(a) and similarly, b is unmatched or prefers a to M(b). While a stable matching in G can be easily computed in linear time by the Gale-Shapley algorithm, it is known that computing a maximum size stable matching is APX-hard. We design an algorithm to give a 1.4667-approximation for the special case where all ties of the preferences appear on the B-side. This algorithm is purely combinatorial and takes only linear time. Per partecipare al Seminario cliccare sul seguente Link: https://bit.ly/3uPLhvf.

## Categorifying Non-Idempotent Intersection Types

 Speaker: Giulio Guerrieri Quando: 19/02/2021 - 15:00 Dove: Online su teams: http://bit.ly/36W271a Abstract Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0. This is joint work with Federico Olimpieri, accepted at CSL 2021.

## On the 24th Hilbert problem and the notion of "simplicity" for proof

 Speaker: Matteo Acclavio Quando: 05/02/2021 - 15:00 Dove: Online su teams al link https://bit.ly/39IhjAI Abstract During the second International Congress of Mathematicians, David Hilbert proposed a list of 23 open problems aiming to inspire the research of 20th-century mathematicians. One century later, a 24th problem has been rediscovered in Hilbert's personal notebook. It can be resumed as follows: -- Is there a criterion to affirm that a certain proof is the "simpler" one? -- In this talk, we will explore this problem: its interpretations and its solutions, emphasizing its impact on 21st-century everyday life.

## The Yoneda Reduction of Polymorphic Types

 Speaker: Paolo Pistone Quando: 29/01/2021 - 15:00 Dove: Online su Teams: https://bit.ly/3qA6qXo Abstract We explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than $\beta\eta$-equivalence, like those induced by parametricity and dinaturality. Based on such isomorphisms, we investigate a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We then demonstrate some applications of this rewriting to problems like counting the inhabitants of a type or characterizing program equivalence in some fragments of System F.

## Intersection Type Distributors

 Speaker: Federico Olimpieri Quando: 15/01/2021 - 15:00 Dove: Videoconferenza su teams al link https://bit.ly/3bbdIMz Abstract Building on previous works, we present a general method to define proof relevant intersection type semantics for pure lambda calculus. We argue that the bicategory of distributors is an appropriate categorical framework for this kind of semantics. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management, following Marsden-Zwardt's approach. We show how these monadic constructions determine Kleisli bicategories over the bicategory of distributors and we give a sufficient condition for cartesian closedness. We define a family of non-extensional models for pure lambda calculus. We then prove that the interpretation of lambda terms induced by these models can be concretely described via intersection type systems. The intersection constructor corresponds to the particular tensor product given by the considered free monadic construction.

## Introduction to FHE and applications to machine learning

 Speaker: Ilaria Chillotti Quando: 18/12/2020 - 15:00 Dove: online su Teams: https://bit.ly/3434DRP Abstract During the talk, we will give a general introduction to Fully Homomorphic Encryption (FHE), a new technology allowing us to perform computations on encrypted data. Then, we will focus on the description of the TFHE scheme, the programmable bootstrapping, and how to use these techniques in a machine learning context. Link to participate on Teams: https://bit.ly/3434DRP

## Stabilization and expansion of simple dynamic random graph models for Bitcoin-like unstructured P2P networks

 Speaker: Francesco Pasquale Quando: 03/07/2020 - 15:00 Dove: videoconferenza online Abstract Venerdì 3 luglio 2020 alle ore 15:00, il prof. Francesco Pasquale dell'Università Tor Vergata, terrà il seminario dal titolo "Stabilization and expansion of simple dynamic random graph models for Bitcoin-like unstructured P2P networks". Abstract The Bitcoin P2P network is formed by thousands of nodes running the Bitcoin protocol. While the nodes participating in the network are mostly known, the peer discovery process in the protocol is explicitly designed to hide the global network structure. In this talk, we present a simple dynamic random graph model inspired by the peer discovery process in the Bitcoin protocol and we analyze its robustness with respect to stabilization and expansion: We show that the network dynamics quickly converges to a stable random graph that turns out to be a good expander, with high probability. The talk is based on joint work with Luca Becchetti, Andrea Clementi, Emanuele Natale, and Luca Trevisan. Per partecipare al seminario cliccare sul seguente link Teams meeting

## Clique is hard on average for regular resolution

 Speaker: Massimo Lauria Quando: 19/06/2020 - 11:30 Dove: videoconferenza online Abstract Venerdì 19 giugno 2020 alle ore 11:30, il prof. Massimo Lauria dell'Università di Roma La Sapienza, presenterà il seminario di Logica e Informatica Teorica dal titolo "Clique is hard on average for regular resolution". Abstract The obvious running time to check whether a graph of n vertices has a clique of size k is roughly n^k. In this work we prove unconditionally that a large variety of state-of-the-art algorithms, even some that are widely used in practice, require running time n^Omega(k). More precisely we prove that for k ≤ n^0.25 regular resolution proofs (i.e. read-once branching programs) have to be of size n^Omega(k) to establish that an Erdos-Rényi graph with appropriately chosen edge density does not contain a k-clique. We remark that these lower bounds do not depend on unproved assumptions like P vs NP, and apply to whatever algorithm that, on k-clique free graphs, produces a regular resolution proofs of such fact. The talk is based on a joint work appeared at STOC 2018, with: Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Jakob Nordström and Alexander A. Razborov. Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams meeting