System crash recovery

Dear all,
last week the server hosting this web page has suffered a drastic (hardware) failure, and it has been re-installed from scratch. Long story short, now is back online, some data have been recovered from backups, but unfortunately we have lost all changes and updates done during August and September. I will re-do them as soon as possible.

Assenza 21 luglio – 1 agosto

Per gli studenti e i tesisti: sarò assente per ferie dal 21 luglio al 1º agosto 2014. In tale periodo sarò in sede solo il 24 o il 25 luglio, per l’appello estivo di laurea. Inoltre non ci sarò il 16-17 luglio per missione a Roma. Pertanto:

  • i tesisti che vogliono tentare gli appelli di laurea della sessione autunnale (ottobre-dicembre) vengano a farsi firmare le carte entro il 18 luglio;
  • gli studenti di Sistemi Distribuiti che vogliano iniziare il loro esame-progetto, se lo facciano assegnare entro il 15 luglio.

Seminario Filippo Bonchi su “Coinduction Up-To (and some applications to equivalence checking)”

Mercoledì 28 maggio alle 9:30 in Sala Riunioni del DiMI, il dott. Filippo Bonchi, Chargé de Recherche CNRS presso l’Ecole Normale Supérieure di Lione, terrà il seguente seminario riguardante recenti suoi risultati:

Coinduction Up-To (and some applications to equivalence checking)

Abstract: Coinduction proof principles, and their enhancements by means of up-to techniques, are widely used for reasoning about automata and processes. In this talk, I will consider bisimulation up-to congruence as a technique for proving language equivalence of non-deterministic finite automata. This technique can be effectively implemented in an algorithm that exponentially improves the state of the art.

Tutti gli interessati sono invitati a partecipare.

Seminario-esame di Teoria delle Categorie: Marco Peressotti

Marco Peressotti terrà il seminario-esame per il Corso di Introduzione alla Teoria delle Categorie il giorno giovedì 8 maggio 2014, con inizio alle ore 14.30, presso la Sala Riunioni del DIMI.
Peressotti ci parlerà di Coalgebraic trace semantics.

Trace semantics has been defined for various kind of state-based systems, notably with different forms of computational behavior/branching such as non-determinism or probabilism.
In the last years a coalgebraic understanding of trace semantics has emerged shading light on the shared mathematical structure behind all these “trace semantics”, namely coinduction in Kleisli categories.

Tutti gli interessati sono invitati (e gli studenti, obbligati).

LFMTP 2014: 9th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice

LFMTP is a long-standing forum for presenting state-of-the-art techniques and discuss progress in the area of logical frameworks and meta-languages. This workshop brings together designers, implementers, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process.

This year, LFMTP is affiliated with CSL-LICS 2014 and IJCAR 2014 and held as part of the Federated Logic Conference (FLoC) and the Vienna Summer of Logic (VSL).


  • Paper Submission: May 2
  • Notification: June 3
  • Final papers due: June 19
  • Workshop: July 17

More details are on the LFMTP workshop web page.