Thérèse Hardin

CoRR, 2009

Development of a Generic Voter under FoCal.

[BibT_eX]

[DOI]

Philippe Ayrault

François Pessaux

Proceedings of the Tests and Proofs - 3rd International Conference, 2009

2008

Development Life-cycle of Critical Software Under FoCaL.

[BibT_eX]

[DOI]

Philippe Ayrault

François Pessaux

Proceedings of the 2nd International Workshop on Harnessing Theories for Tool Support in Software, 2008

A Few Remarks about Formal Development of Secure Systems.

[BibT_eX]

[DOI]

Éric Jaeger

Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium, 2008

2007

On the Implementation of Construction Functions for Non-free Concrete Data Types.

[BibT_eX]

[DOI]

Frédéric Blanqui

Pierre Weis

Proceedings of the Programming Languages and Systems, 2007

2004

Les objets des mathématiques.

[BibT_eX]

[DOI]

Renaud Rioboo

Obj. Logiciel Base données Réseaux, 2004

Building certified components within FOCAL.

[BibT_eX]

Catherine Dubois

Véronique Donzeau-Gouge

Proceedings of the Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, 2004

2003

Theorem Proving Modulo.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

2002

Algebraic Structures and Dependent Records.

[BibT_eX]

[DOI]

Virgile Prevosto

Damien Doligez

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Binding Logic: Proofs and Models.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2002

2001

HOL-λσ: an intentional first-order expression of higher-order logic.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2001

2000

Higher Order Unification via Explicit Substitutions.

[BibT_eX]

[DOI]

Inf. Comput., 2000

1999

On the way to certify Computer Algebra Systems.

[BibT_eX]

[DOI]

Sylvain Boulmé

Daniel Hirschkoff

Valérie Ménissier-Morain

Renaud Rioboo

Proceedings of the Systems for Integrated Computation and Deduction, 1999

HOL-<i>lambdasigma</i>: An Intentional First-Order Expression of Higher-Order Logic.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

1998

Functional Runtime Systems Within the Lambda-Sigma Calculus.

[BibT_eX]

[DOI]

Luc Maranget

J. Funct. Program., 1998

1996

Strong Normalizations of Substitutions.

[BibT_eX]

[DOI]

Alejandro Ríos

J. Log. Comput., 1996

Confluence Properties of Weak and Strong Calculi of Explicit Substitutions.

[BibT_eX]

[DOI]

Jean-Jacques Lévy

J. ACM, 1996

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.

[BibT_eX]

[DOI]

Proceedings of the Logic Programming, 1996

Functional Back-Ends within the Lambda-Sigma Calculus.

[BibT_eX]

[DOI]

Luc Maranget

Bruno Pagano

Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, 1996

1995

Eta-conversion for the languages of explicit substitutions.

[BibT_eX]

[DOI]

Appl. Algebra Eng. Commun. Comput., 1995

Higher-Order Unification via Explicit Substitutions (Extended Abstract)

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1995

1994

Yet Yet a Counterexample for lambda + SP.

[BibT_eX]

[DOI]

J. Funct. Program., 1994

1992

Strong Normalization of Substitutions.

[BibT_eX]

[DOI]

Alejandro Ríos

Proceedings of the Mathematical Foundations of Computer Science 1992, 1992

1989

Confluence Results for the Pure Strong Categorical Logic CCL: lambda-Calculi as Subsystems of CCL.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1989

1986

Proof of termination of the rewriting system subst on CCL.

[BibT_eX]

[DOI]