2009 |
26 | EE | Éric Jaeger,
Thérèse Hardin:
A Few Remarks About Formal Development of Secure Systems
CoRR abs/0902.3861: (2009) |
25 | EE | Éric Jaeger,
Thérèse Hardin:
Yet Another Deep Embedding of B:Extending de Bruijn Notations
CoRR abs/0902.3865: (2009) |
2008 |
24 | EE | Éric Jaeger,
Thérèse Hardin:
A Few Remarks about Formal Development of Secure Systems.
HASE 2008: 165-174 |
2007 |
23 | EE | Frédéric Blanqui,
Thérèse Hardin,
Pierre Weis:
On the Implementation of Construction Functions for Non-free Concrete Data Types.
ESOP 2007: 95-109 |
22 | EE | Frédéric Blanqui,
Thérèse Hardin,
Pierre Weis:
On the implementation of construction functions for non-free concrete data types
CoRR abs/cs/0701031: (2007) |
2004 |
21 | | Catherine Dubois,
Thérèse Hardin,
Véronique Donzeau-Gouge:
Building certified components within FOCAL.
Trends in Functional Programming 2004: 33-48 |
20 | EE | Thérèse Hardin,
Renaud Rioboo:
Les objets des mathématiques.
L'OBJET 10(4): 83-118 (2004) |
2003 |
19 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Theorem Proving Modulo.
J. Autom. Reasoning 31(1): 33-72 (2003) |
2002 |
18 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Binding Logic: Proofs and Models.
LPAR 2002: 130-144 |
17 | EE | Virgile Prevosto,
Damien Doligez,
Thérèse Hardin:
Algebraic Structures and Dependent Records.
TPHOLs 2002: 298-313 |
2001 |
16 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
HOL-[lambda][sigma]: an intentional first-order expression of higher-order logic.
Mathematical Structures in Computer Science 11(1): 21-45 (2001) |
2000 |
15 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Higher Order Unification via Explicit Substitutions.
Inf. Comput. 157(1-2): 183-235 (2000) |
1999 |
14 | EE | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic.
RTA 1999: 317-331 |
13 | EE | Sylvain Boulmé,
Thérèse Hardin,
Daniel Hirschkoff,
Valérie Ménissier-Morain,
Renaud Rioboo:
On the way to certify Computer Algebra Systems.
Electr. Notes Theor. Comput. Sci. 23(3): (1999) |
1998 |
12 | | Thérèse Hardin,
Luc Maranget:
Functional Runtime Systems Within the Lambda-Sigma Calculus.
J. Funct. Program. 8(2): 131-176 (1998) |
1996 |
11 | | Thérèse Hardin,
Luc Maranget,
Bruno Pagano:
Functional Back-Ends within the Lambda-Sigma Calculus.
ICFP 1996: 25-33 |
10 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner,
Frank Pfenning:
Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
JICSLP 1996: 259-273 |
9 | EE | 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): 362-397 (1996) |
8 | | Pierre-Louis Curien,
Thérèse Hardin,
Alejandro Ríos:
Strong Normalizations of Substitutions.
J. Log. Comput. 6(6): 799-817 (1996) |
1995 |
7 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner:
Higher-Order Unification via Explicit Substitutions (Extended Abstract)
LICS 1995: 366-374 |
6 | EE | Thérèse Hardin:
Eta-Conversion for Languages of Explicit Substitutions.
Appl. Algebra Eng. Commun. Comput. 6(4/5): 325 (1995) |
1994 |
5 | | Thérèse Hardin:
Eta-Conversion for the Languages of Explicit Substitutions.
Appl. Algebra Eng. Commun. Comput. 5: 317-341 (1994) |
4 | | Pierre-Louis Curien,
Thérèse Hardin:
Yet Yet a Counterexample for lambda + SP.
J. Funct. Program. 4(1): 113-115 (1994) |
1992 |
3 | | Thérèse Hardin:
Eta-conversion for the Languages of Explicit Substitutions.
ALP 1992: 306-321 |
2 | | Pierre-Louis Curien,
Thérèse Hardin,
Alejandro Ríos:
Strong Normalization of Substitutions.
MFCS 1992: 209-217 |
1989 |
1 | | Thérèse Hardin:
Confluence Results for the Pure Strong Categorical Logic CCL: lambda-Calculi as Subsystems of CCL.
Theor. Comput. Sci. 65(3): 291-342 (1989) |