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

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


Compositional theories for embedded programming

Speaker:
Margherita Zorzi
Quando:
26/06/2020 - 15:00
Dove:
videoconferenza online
Abstract

Venerdì 26 giugno 2020 alle ore 15:00, la prof.ssa Margherita Zorzi dell'Università di Verona, presenterà il seminario di Logica e Informatica Teorica dal titolo "Compositional theories for embedded programming".

Abstract:

Embedded programming style allows to split the syntax in two parts, representing respectively a host language H and a core language C embedded in H. This formally models several situations in which a user writes code in a main language and delegates some tasks to an ad hoc domain specific language. Moreover, as showed in recent years, a particular case of the host-core approach allows a flexible management of data linearity, which is particularly useful in non-classical computational paradigms such as quantum computing. The definition of a systematised type theory to capture and standardize common properties of embedded languages is partially unexplored. We present a flexible fragment of such a type theory, together with its semantics in terms of enriched categories. We introduce the calculus HC0 and we use the notion of internal language of a category to relate the language to the class of its models, showing the equivalence between the category of models and the one of theories. This provides a stronger result w.r.t. standard soundness and completeness since it involves not only the models but also morphisms between models. We observe that the definition of the morphisms between models highlights further advantages of the embedded languages and we discuss some concrete instances, extensions and specializations of the syntax and the semantics.

Per partecipare al seminario, richiedere il link all’indirizzo email vitomichele.abrusci@uniroma3.it o cliccare sul seguente link Teams meeting