Equality Is Typable in Semi-full Pure Type Systems. - Vincent Siles; Hugo Herbelin (LICS, 2010)

Investigation on the typing of equality in type systems. (Etude sur le typage de l'égalité dans les systèmes de types). - Vincent Siles (2010)

A Decision Procedure for Regular Expression Equivalence in Type Theory. - Thierry Coquand; Vincent Siles (CPP, 2011)

Coherent and Strongly Discrete Rings in Type Theory. - Thierry Coquand; Anders Mörtberg; Vincent Siles (CPP, 2012)

Towards a Certified Computation of Homology Groups for Digital Images. - Jónathan Heras; Maxime Dénès; Gadea Mata; Anders Mörtberg; María Poza; Vincent Siles (CTIC, 2012)

A Refinement-Based Approach to Computational Algebra in Coq. - Maxime Dénès; Anders Mörtberg; Vincent Siles (ITP, 2012)

Pure Type System conversion is always typable. - Vincent Siles; Hugo Herbelin (J. Funct. Program., 2012)

A formal proof of Sasaki-Murao algorithm. - Thierry Coquand; Anders Mörtberg; Vincent Siles (J. Formaliz. Reason., 2012)

Computing persistent homology within Coq/SSReflect. - Jónathan Heras; Thierry Coquand; Anders Mörtberg; Vincent Siles (ACM Trans. Comput. Log., 2013)

Modeling and Abstraction of Memory Management in a Hypervisor. - Pauline Bolignano; Thomas Jensen; Vincent Siles (FASE, 2016)

Formalized linear algebra over Elementary Divisor Rings in Coq. - Guillaume Cano; Cyril Cohen; Maxime Dénès; Anders Mörtberg; Vincent Siles (Log. Methods Comput. Sci., 2016)