The B-Book. Assigning programs to meaning. C a m bridge University Press, 1996. ,
Veriication of sequential and concurrent programs, 1991. ,
The Coq P r oof Assistant Reference Manual Version 6, 1996. ,
The Calculus of Constructions. Information and Computation, vol.76, 1988. ,
URL : https://hal.archives-ouvertes.fr/inria-00076024
Functional translation of imperative programs ,
, Proofs and Types, 1989.
Speciication Case Studies, 1985. ,
An axiomatic basis for computer programming, 576{580,583, vol.12, 1969. ,
Systematic Software Development using VDM, 1989. ,
, Introduction to Metamathematics. Bibliotheca Mathematica, 1952.
From Algol to Polymorphic Linear Lambda-calculus, 1997. ,
Developing certiied programs in the system Coq { The Program tactic, Proceedings of the BRA Workshop Types for Proofs and Programs, vol.9, p.3, 1993. ,
Extracting F ! 's programs from proofs in the Calculus of Constructions, Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989. ,
, Proceedings of the conference T yped L ambda Calculi and Applications, n umber 664 in LNCS, 1993. Also LIP research report, pp.92-141
The KIV-approach t o S o f t ware Veriication, KORSO: Methods, Languages, and Tools for the Construction of Correct Software { Final Report. Springer LNCS 1009, 1995. ,
Auxiliary variables and recursive procedures, TAPSOFT'97: Theory and Practice of Software Development, v olume 1214 of Lecture Notes in Computer Science, pp.697-711, 1997. ,