Some Experiments in Certified Software
Joëlle Despeyroux
I've done many short developments, in the Coq system, on
specifications of various languages, and proofs of different
properties of them: preservation of types (also called Subject
Reduction Theorem), proof of correctness of compilers, certified
algorithms for inference of types, etc...
Some of these experiments
have been done in joint works with Phd students or students coming for
a couple of months, during the summer.
The languages concerned are:
a simple imperative language with procedures, various description of Mini-ML,
the pi-calculus, some object calculi some of them based on the pi-calculus,
etc...
Some of my papers reporting on experiments in certified software
(please contact me if you are interested in any unpublished drafts) :
-
A Higher-order specification of the pi-calculus
(draft version).
To appear in the proc. of the IFIP International Conference on
Theoretical Computer Science, IFIP TCS'2000, Sendai, Japan, August
17-19, 2000.
-
Sémantique Naturelle: Spécifications et Preuves,
INRIA research report
RR-3359, February 1998.
Lecture notes of a graduate course in the "DEA" "Mathématiques Discrètes et
Fondements de l'Informatique" (MDFI), Marseille, 1995-1999
(85 pages, in french).
-
Higher-order abstract syntax in Coq,
Joint work with Amy Felty, and André Hirschowitz.
2nd int. conf. on
Typed Lambda-Calculi and Applications, TLCA'95,
Edinburgh, April 1995. Springer-Verlag LNCS 902.
Also appears as INRIA research report RR-2556, April 1995.
-
Higher-order Syntax and Induction in Coq,
Joint work with André Hirschowitz.
Fifth Int. Conf. on Logic Programming and Automated Reasoning, LPAR,
Kiev, July 1994. Springer-Verlag LNAI 822.
Also appears as INRIA research report RR-2292, June 1994.
-
Theo: An Interactive Proof Development System,
in a special issue on Programming Logic ,
the Scandinavian Journal on Computer Science and Numerical Analysis
BIT (32), pp 15-29, 1992.
-
Theo: An Interactive Proof Development System. User's manual,
INRIA technical report RT-116, February 1990.
-
Current experiments in Natural Semantics,
Joint work with Thierry Despeyroux.
the MCC-INRIA conference
on the Resolution of Equations in Algebraic Structures ,
Lakeway, Texas, May 1987.
-
Proof of translation in Natural Semantics,
first Symp. on Logic In Computer Science ,
LICS, Cambridge, Ma, USA, June 1986.
Also appears as INRIA research report RR 514, April 1986.
-
A Simple Applicative Language: Mini-ML,
Joint work with D. Clement, Th. Despeyroux and G. Kahn.
the ACM conference Lisp and Functional Programming ,
L&FP, Cambridge, Ma, USA, August 1986.
Also available as an INRIA research report RR-529, May 1986.June 1986.
-
Natural Semantics on the Computer,
Joint work with D. Clement Th. Despeyroux and G. Kahn.
INRIA research report RR-416, June 1985.
-
An algebraic specification of a Pascal Compiler,
ACM Sigplan Notices , vol. 18, nb 12, Dec. 83, pages 34-48.
Also available as an INRIA research report RR-209, May 1983.
Joint works with PhD students:
-
Guillaume Gillard started his PhD thesis in October 97.
Formal Specifications of Properties of Concurrent Object Languages.
- Delphine Kaplan-Terrasse
completed her PhD
thesis in 95:
Towards an Environment for the Development of Proofs in Natural Semantics.
She has then proved the
correctness
of a subtental part of the Esterel compiler.
She is now assistant professor at Eurecom.
Joint works with Master students, in the Coq system:
Joëlle Despeyroux