Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. - Benedikt Ahrens; Régis Spadotti (TYPES, 2014)

Coinitial semantics for redecoration of triangular matrices. - Benedikt Ahrens; Régis Spadotti (CoRR, 2014)

A Mechanized Theory of Regular Trees in Dependent Type Theory. - Régis Spadotti (ITP, 2015)

Non-Wellfounded Trees in Homotopy Type Theory. - Benedikt Ahrens; Paolo Capriotti; Régis Spadotti (TLCA, 2015)

Towards a verified transformation from AADL to the formal component-based language FIACRE. - Jean-Paul Bodeveix; Mamoun Filali; Manuel Garnacho; Régis Spadotti; Zhibin Yang (Sci. Comput. Program., 2015)

A mechanized theory of regular trees in dependent type theory. (Une théorie mécanisée des arbres réguliers en théorie des types dépendants). - Régis Spadotti (2016)