Christine Paulin-Mohring

24 papers A* 1B 6Journal 5Unranked 7
YearRankTypeTitle / Venue / Authors
2025 J jnl
When Proofs Meet Programs: An Extension of Dependent Type Theory with Church's Thesis.
Commun. ACM
Christine Paulin-Mohring
2013 B ed.
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings
ITP
Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
2012 B conf
Towards Provably Robust Watermarking.
ITP
David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring
2011 — conf
Introduction to the Coq Proof-Assistant for Practical Software Verification.
LASER Summer School
Christine Paulin-Mohring
2011 J jnl
Preface.
Sci. Comput. Program.
Philippe Audebaud, Christine Paulin-Mohring
2009 J jnl
Proofs of randomized algorithms in Coq.
Sci. Comput. Program.
Philippe Audebaud, Christine Paulin-Mohring
2008 B ed.
Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings
MPC
Philippe Audebaud, Christine Paulin-Mohring
2006 B conf
Proofs of Randomized Algorithms in Coq.
MPC
Philippe Audebaud, Christine Paulin-Mohring
2006 — ed.
Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers
TYPES
Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner
2005 B conf
Formal Verification of Security Properties of Smart Card Embedded Source Code.
FM
June Andronick, Boutheina Chetali, Christine Paulin-Mohring
2005 — conf
Reasoning About Java Programs with Aliasing and Frame Conditions.
TPHOLs
Claude Marché, Christine Paulin-Mohring
2004 J jnl
The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML.
J. Log. Algebraic Methods Program.
Claude Marché, Christine Paulin-Mohring, Xavier Urbain
2001 — conf
Modelisation of Timed Automata in Coq.
TACS
Christine Paulin-Mohring
1999 — ed.
Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings
TPHOLs
Yves Bertot, Gilles Dowek, André Hirschowitz, Christine Paulin-Mohring, Laurent Théry
1998 — ed.
Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers
TYPES
Eduardo Giménez, Christine Paulin-Mohring
1996 — book
Définitions Inductives en Théorie des Types. (Inductive Definitions in Type Theory).
Christine Paulin-Mohring
1996 — conf
Introduction.
TYPES
Eduardo Giménez, Christine Paulin-Mohring
1995 — conf
Circuits as Streams in Coq: Verification of a Sequential Multiplier.
TYPES
Christine Paulin-Mohring
1993 — conf
Inductive Definitions in the system Coq - Rules and Properties.
TLCA
Christine Paulin-Mohring
1993 — conf
Programming with Streams in Coq - A Case Study: the Sieve of Eratosthenes.
TYPES
François Leclerc, Christine Paulin-Mohring
1993 J jnl
Synthesis of ML Programs in the System Coq.
J. Symb. Comput.
Christine Paulin-Mohring, Benjamin Werner
1989 A* conf
Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions.
POPL
Christine Paulin-Mohring
1989 — —
Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions).
Christine Paulin-Mohring
1989 B conf
Inductively Defined Types in the Calculus of Constructions.
Mathematical Foundations of Programming Semantics
Frank Pfenning, Christine Paulin-Mohring