A Weak Calculus with Explicit Operators for Pattern Matching and Substitution. - Julien Forest (RTA, 2002)

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. - Gilles Barthe; Julien Forest; David Pichardie; Vlad Rusu (FLOPS, 2006)

Certification of Automated Termination Proofs. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (FroCoS, 2007)

Expression Reduction Systems with Patterns. - Julien Forest; Delia Kesner (J. Autom. Reason., 2007)

Certifying a Termination Criterion Based on Graphs, without Graphs. - Pierre Courtieu; Julien Forest; Xavier Urbain (TPHOLs, 2008)

ShareX3D, a scientific collaborative 3D viewer over HTTP. - Sébastien Jourdain; Julien Forest; Christophe Mouton; Bernard Nouailhas; Gerard Moniot; Franck Kolb; Sophie Chabridon; Michel Simatic; Zied Abid; Laurent Mallet (Web3D, 2008)

A3PAT, an approach for certified automated termination proofs. - Evelyne Contejean; Andrey Paskevich; Xavier Urbain; Pierre Courtieu; Olivier Pons; Julien Forest (PEPM, 2010)

Structural Analysis of Narratives with the Coq Proof Assistant. - Anne-Gwenn Bosser; Pierre Courtieu; Julien Forest; Marc Cavazza (ITP, 2011)

Automated Certified Proofs with CiME3. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (RTA, 2011)