A functional functional interpretation. - Pierre-Marie Pédrot (CSL-LICS, 2014)

Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse. - Pierre-Marie Pédrot; Amina Doumane; Alexis Saurin (JFLA, 2014)

A Materialist Dialectica. (Une Dialectica matérialiste). - Pierre-Marie Pédrot (2015)

Classical By-Need. - Pierre-Marie Pédrot; Alexis Saurin (ESOP, 2016)

The Definitional Side of the Forcing. - Guilhem Jaber; Gabriel Lewertowski; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau (LICS, 2016)

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

An effectful way to eliminate addiction to dependence. - Pierre-Marie Pédrot; Nicolas Tabareau (LICS, 2017)

Failure is Not an Option - An Exceptional Type Theory. - Pierre-Marie Pédrot; Nicolas Tabareau (ESOP, 2018)

A reasonably exceptional type theory. - Pierre-Marie Pédrot; Nicolas Tabareau; Hans Jacob Fehrmann; Éric Tanter (Proc. ACM Program. Lang., 2019)

Russian Constructivism in a Prefascist Theory. - Pierre-Marie Pédrot (LICS, 2020)

The fire triangle: how to mix substitution, dependent elimination, and effects. - Pierre-Marie Pédrot; Nicolas Tabareau (Proc. ACM Program. Lang., 2020)

Extending the team with a project-specific bot. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (CoRR, 2021)

Gardening with the Pythia A Model of Continuity in a Dependent Setting. - Martin Baillon; Assia Mahboubi; Pierre-Marie Pédrot (CSL, 2022)

Advantages of maintaining a multi-task project-specific bot: an experience report. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (CoRR, 2022)

The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report. - Théo Zimmermann; Julien Coolen; Jason Gross; Pierre-Marie Pédrot; Gaëtan Gilbert (IEEE Softw., 2022)

Martin-Löf à la Coq. - Arthur Adjedj; Meven Lennon-Bertrand; Kenji Maillard; Pierre-Marie Pédrot; Loïc Pujet (CPP, 2024)

δ is for Dialectica. - Marie Morgane Kerjean; Pierre-Marie Pédrot (LICS, 2024)

A Zoo of Continuity Properties in Constructive Type Theory. - Martin Baillon; Yannick Forster 002; Assia Mahboubi; Pierre-Marie Pédrot; Matthieu Piquerez (FSCD, 2025)

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants. - Josselin Poiret; Gaëtan Gilbert; Kenji Maillard; Pierre-Marie Pédrot; Matthieu Sozeau; Nicolas Tabareau; Éric Tanter (Proc. ACM Program. Lang., 2025)

'Upon This Quote I Will Build My Church Thesis'. - Pierre-Marie Pédrot (Commun. ACM, 2025)