The next 700 syntactical models of type theory. - Simon Boulier; Pierre-Marie Pédrot; Nicolas Tabareau (CPP, 2017)

Towards Certified Meta-Programming with Typed Template-Coq. - Abhishek Anand; Simon Boulier; Cyril Cohen; Matthieu Sozeau; Nicolas Tabareau (ITP, 2018)

Extending type theory with syntactic models. (Etendre la théorie des types à l'aide de modèles syntaxiques). - Simon Pierre Boulier (2018)

Setoid Type Theory - A Syntactic Translation. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Nicolas Tabareau (MPC, 2019)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

Coq Coq correct! verification of type checking and erasure for Coq, in Coq. - Matthieu Sozeau; Simon Boulier; Yannick Forster 002; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2020)

Constructing a universe for the setoid model. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Christian Sattler; Filippo Sestini (FoSSaCS, 2021)

Model structure on the universe of all types in interval type theory. - Simon Boulier; Nicolas Tabareau (Math. Struct. Comput. Sci., 2021)