Thérèse Hardin

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