Proof of termination of the rewriting system subst on CCL. - Thérèse Hardin; Alain Laville (Theor. Comput. Sci., 1986)

Confluence Results for the Pure Strong Categorical Logic CCL: lambda-Calculi as Subsystems of CCL. - Thérèse Hardin (Theor. Comput. Sci., 1989)

Strong Normalization of Substitutions. - Pierre-Louis Curien; Thérèse Hardin; Alejandro Ríos 001 (MFCS, 1992)

Yet Yet a Counterexample for lambda + SP. - Pierre-Louis Curien; Thérèse Hardin (J. Funct. Program., 1994)

Higher-Order Unification via Explicit Substitutions (Extended Abstract) - Gilles Dowek; Thérèse Hardin; Claude Kirchner (LICS, 1995)

Eta-conversion for the languages of explicit substitutions. - Thérèse Hardin (Appl. Algebra Eng. Commun. Comput., 1995)

Functional Back-Ends within the Lambda-Sigma Calculus. - Thérèse Hardin; Luc Maranget; Bruno Pagano (ICFP, 1996)

Unification via Explicit Substitutions: The Case of Higher-Order Patterns. - Gilles Dowek; Thérèse Hardin; Claude Kirchner; Frank Pfenning (JICSLP, 1996)

Confluence Properties of Weak and Strong Calculi of Explicit Substitutions. - Pierre-Louis Curien; Thérèse Hardin; Jean-Jacques Lévy (J. ACM, 1996)

Strong Normalizations of Substitutions. - Pierre-Louis Curien; Thérèse Hardin; Alejandro Ríos 001 (J. Log. Comput., 1996)

Functional Runtime Systems Within the Lambda-Sigma Calculus. - Thérèse Hardin; Luc Maranget (J. Funct. Program., 1998)

HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (RTA, 1999)

On the way to certify Computer Algebra Systems. - Sylvain Boulmé; Thérèse Hardin; Daniel Hirschkoff; Valérie Ménissier-Morain; Renaud Rioboo (Calculemus, 1999)

Higher Order Unification via Explicit Substitutions. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (Inf. Comput., 2000)

HOL-λσ: an intentional first-order expression of higher-order logic. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (Math. Struct. Comput. Sci., 2001)

Binding Logic: Proofs and Models. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (LPAR, 2002)

Algebraic Structures and Dependent Records. - Virgile Prevosto; Damien Doligez; Thérèse Hardin (TPHOLs, 2002)

Theorem Proving Modulo. - Gilles Dowek; Thérèse Hardin; Claude Kirchner (J. Autom. Reason., 2003)

Building certified components within FOCAL. - Catherine Dubois; Thérèse Hardin; Véronique Donzeau-Gouge (Trends in Functional Programming, 2004)

Les objets des mathématiques. - Thérèse Hardin; Renaud Rioboo (Obj. Logiciel Base données Réseaux, 2004)

On the Implementation of Construction Functions for Non-free Concrete Data Types. - Frédéric Blanqui; Thérèse Hardin; Pierre Weis (ESOP, 2007)

A Few Remarks about Formal Development of Secure Systems. - Éric Jaeger; Thérèse Hardin (HASE, 2008)

Development Life-cycle of Critical Software Under FoCaL. - Philippe Ayrault; Thérèse Hardin; François Pessaux (TTSS, 2008)

Development of a Generic Voter under FoCal. - Philippe Ayrault; Thérèse Hardin; François Pessaux (TAP@TOOLS, 2009)

Yet Another Deep Embedding of B:Extending de Bruijn Notations - Éric Jaeger; Thérèse Hardin (CoRR, 2009)

Experience in using a typed functional language for the development of a security application. - Damien Doligez; Christèle Faure; Thérèse Hardin; Manuel Maarek (F-IDE, 2014)

Avoiding Security Pitfalls with Functional Programming: A Report on the Development of a Secure XML Validator. - Damien Doligez; Christèle Faure; Thérèse Hardin; Manuel Maarek (ICSE (2), 2015)