Thérèse Hardin

Publication Activity (10 Years)

Years Active: 1986-2023
Publications (10 Years): 2

Top Topics

Functional Language

Top Venues

Publications

Gilles Dowek, Thérèse Hardin, Claude Kirchner
Binding Logic: proofs and models. CoRR (2023)
Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek
Avoiding Security Pitfalls with Functional Programming: A Report on the Development of a Secure XML Validator. ICSE (2) (2015)
Damien Doligez, Christèle Faure, Thérèse Hardin, Manuel Maarek
Experience in using a typed functional language for the development of a security application. F-IDE (2014)
Éric Jaeger, Thérèse Hardin
Yet Another Deep Embedding of B:Extending de Bruijn Notations CoRR (2009)
Philippe Ayrault, Thérèse Hardin, François Pessaux
Development of a Generic Voter under FoCal. TAP@TOOLS (2009)
Philippe Ayrault, Thérèse Hardin, François Pessaux
Development Life-cycle of Critical Software Under FoCaL. Electron. Notes Theor. Comput. Sci. 243 (2009)
Éric Jaeger, Thérèse Hardin
A Few Remarks About Formal Development of Secure Systems CoRR (2009)
Éric Jaeger, Thérèse Hardin
A Few Remarks about Formal Development of Secure Systems. HASE (2008)
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
On the Implementation of Construction Functions for Non-free Concrete Data Types. ESOP (2007)
Frédéric Blanqui, Thérèse Hardin, Pierre Weis
On the implementation of construction functions for non-free concrete data types CoRR (2007)
Thérèse Hardin, Renaud Rioboo
Les objets des mathématiques. Obj. Logiciel Base données Réseaux 10 (4) (2004)
Catherine Dubois, Thérèse Hardin, Véronique Donzeau-Gouge
Building certified components within FOCAL. Trends in Functional Programming (2004)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
Theorem Proving Modulo. J. Autom. Reason. 31 (1) (2003)
Virgile Prevosto, Damien Doligez, Thérèse Hardin
Algebraic Structures and Dependent Records. TPHOLs (2002)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
Binding Logic: Proofs and Models. LPAR (2002)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
HOL-λσ: an intentional first-order expression of higher-order logic. Math. Struct. Comput. Sci. 11 (1) (2001)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
Higher Order Unification via Explicit Substitutions. Inf. Comput. 157 (1-2) (2000)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
: An Intentional First-Order Expression of Higher-Order Logic. RTA (1999)
Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo
On the way to certify Computer Algebra Systems. Calculemus (1999)
Thérèse Hardin, Luc Maranget
Functional Runtime Systems Within the Lambda-Sigma Calculus. J. Funct. Program. 8 (2) (1998)
Thérèse Hardin, Luc Maranget, Bruno Pagano
Functional Back-Ends within the Lambda-Sigma Calculus. ICFP (1996)
Pierre-Louis Curien, Thérèse Hardin, Alejandro Ríos
Strong Normalizations of Substitutions. J. Log. Comput. 6 (6) (1996)
Pierre-Louis Curien, Thérèse Hardin, Jean-Jacques Lévy
Confluence Properties of Weak and Strong Calculi of Explicit Substitutions. J. ACM 43 (2) (1996)
Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning
Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP (1996)
Gilles Dowek, Thérèse Hardin, Claude Kirchner
Higher-Order Unification via Explicit Substitutions (Extended Abstract) LICS (1995)
Thérèse Hardin
Eta-conversion for the languages of explicit substitutions. Appl. Algebra Eng. Commun. Comput. 6 (4/5) (1995)
Thérèse Hardin
Eta-Conversion for the Languages of Explicit Substitutions. Appl. Algebra Eng. Commun. Comput. 5 (1994)
Pierre-Louis Curien, Thérèse Hardin
Yet Yet a Counterexample for lambda + SP. J. Funct. Program. 4 (1) (1994)
Thérèse Hardin
Eta-conversion for the Languages of Explicit Substitutions. ALP (1992)
Pierre-Louis Curien, Thérèse Hardin, Alejandro Ríos
Strong Normalization of Substitutions. MFCS (1992)
Thérèse Hardin
Confluence Results for the Pure Strong Categorical Logic CCL: lambda-Calculi as Subsystems of CCL. Theor. Comput. Sci. 65 (3) (1989)
Thérèse Hardin, Alain Laville
Proof of termination of the rewriting system subst on CCL. Theor. Comput. Sci. 46 (1986)