
My principal line of research is the study of the integration of XMLbased Mathematical Knowledge Management technologies with Interactive Theorem Proving.
More generally, I am interested in:
Code (in C#) for the paper "Sharing Equivalence is Linear".
Author: Emanuele Sinagra under the supervision of Claudio Sacerdoti Coen.
The code implements:
Two nodes are sharing equivalent when their readbacks as λterms of the subDAG rooted in them are αconvertible. The precondition of the algorithm is that the set of pairs must respect the wellscoped property, i.e. when a node in the pair can reach a variable and is in the scope of the binder of the variable, then the other term must be too.
The code can also output a detailed representation of the state of the algorithm after every step. Look here for an example run.
A detailed proof of soundness and completeness can be found in: B. Accattoli, A. Condoluci, C. Sacerdoti Coen. "Sharing Equivalence is Linear" Submitted to LICS 2018.
Since the academic year 20172018 I am teaching Emerging Programming Paradigms ("Paradigmi di Programmazione Emergenti"). The teaching material (in Italian only) can be found here.
Since the academic year 20152016 I am teaching a module of Logic Foundations of Computer Science ("Fondamenti Logici per l'Informatica"). The teaching material (in Italian only) can be found here.
Since the academic year 20122013 I am teaching Logic ("Logica per l'informatica"). The teaching material (in Italian only) can be found here.
In the academic year 20142015 I tought a module of the Algorithm and Data Structure course ("Algoritmi e Strutture Dati"). The teaching material (in Italian only) can be found here.
In the academic year 20162017 I tought a module of the Algorithm and Data Structure course at the Master Degree in Bioinformatics. The teaching material can be found here.
In the academic year 20102011 I tought a short course on constructive mathematics to the students of the Collegio d'Eccellenza. The teaching material (in Italian only) can be found here.
In the academic years 200820011 I used to teach Languages and Structures ("Linguaggi e Strutture"), which is an introduction to logic and algebra. The teaching material (in Italian only) can be found here.
In the academic years 20052006, 20062007 and 20072008 I used to teach Operating Systems ("Sistemi Operativi [MZ]") and, in 200720008 only, also the associated Laboratory ("Laboratorio di Sistemi Operativi [MZ]"). All the teachning material related to it (in Italian only) can be found here.