Inductively Defined Types in the Calculus of Constructions. - Frank Pfenning; Christine Paulin-Mohring (Mathematical Foundations of Programming Semantics, 1989)

Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions. - Christine Paulin-Mohring (POPL, 1989)

Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions). - Christine Paulin-Mohring (1989)

Inductive Definitions in the system Coq - Rules and Properties. - Christine Paulin-Mohring (TLCA, 1993)

Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes. - François Leclerc; Christine Paulin-Mohring (TYPES, 1993)

Synthesis of ML Programs in the System Coq. - Christine Paulin-Mohring; Benjamin Werner (J. Symb. Comput., 1993)

Circuits as Streams in Coq: Verification of a Sequential Multiplier. - Christine Paulin-Mohring (TYPES, 1995)

Définitions Inductives en Théorie des Types. (Inductive Definitions in Type Theory). - Christine Paulin-Mohring (1996)

Introduction. - Eduardo Giménez 001; Christine Paulin-Mohring (TYPES, 1996)

Modelisation of Timed Automata in Coq. - Christine Paulin-Mohring (TACS, 2001)

The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. - Claude Marché; Christine Paulin-Mohring; Xavier Urbain (J. Log. Algebraic Methods Program., 2004)

Formal Verification of Security Properties of Smart Card Embedded Source Code. - June Andronick; Boutheina Chetali; Christine Paulin-Mohring (FM, 2005)

Reasoning About Java Programs with Aliasing and Frame Conditions. - Claude Marché; Christine Paulin-Mohring (TPHOLs, 2005)

Proofs of randomized algorithms in Coq. - Philippe Audebaud; Christine Paulin-Mohring (Sci. Comput. Program., 2009)

Introduction to the Coq Proof-Assistant for Practical Software Verification. - Christine Paulin-Mohring (LASER Summer School, 2011)

Preface. - Philippe Audebaud; Christine Paulin-Mohring (Sci. Comput. Program., 2011)

Towards Provably Robust Watermarking. - David Baelde; Pierre Courtieu; David Gross-Amblard; Christine Paulin-Mohring (ITP, 2012)

When Proofs Meet Programs: An Extension of Dependent Type Theory with Church's Thesis. - Christine Paulin-Mohring (Commun. ACM, 2025)