The Coq Proof Assistant Reference Manual Version 6, Proceedings of TLCA'95, vol.902, 1995. ,
Pruning simply typed ?-terms, 1993. ,
Extending pruning techniques to polymorphic second order ?-calculus, Proceedings of ESOP'94, vol.788, pp.120-134, 1994. ,
Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL '77 ), pp.238-252, 1977. ,
A simple applicative language: Mini-ML, Technical Report, vol.529, 1986. ,
Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial, SAS'95: 2nd Int'l Static Analysis Symposium, vol.983, pp.118-135, 1995. ,
Detecting and removing dead code using rank-2 intersection, International Workshop:"TYPES'96, vol.1512, 1998. ,
, Proofs and Types, 1989.
Control-flow analysis and type systems, Proceeding of SAS 1995, vol.983, pp.189-206, 1995. ,
A type-based framework for program analysis, Proceedings of the Static Analysis Symposium, vol.864, pp.380-394, 1994. ,
Abstract Interpretation of functionnal languages : from theory to Practice, 1991. ,
Lego proof development system : User's manual, 1992. ,
A type inference approach to reduction properties and semantics of polymorphic expressions, Logical Foundations of Functionnal programming, pp.195-211, 1990. ,
Strictness and totality analysis, Static Analysis, vol.864, pp.408-422, 1994. ,
Extraction de programmes dans le calcul des constructions, 1989. ,
URL : https://hal.archives-ouvertes.fr/tel-00431825
Extracting F?'s programs from proofs in the Calculus of Constructions, Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989. ,
Using ML type inference for dead code analysis, 1997. ,
Annotated Type Systems for Program Analysis, 1995. ,
The type and effect discipline, Proceedings of the 1992 Conference on Logic in Computer Science, 1992. ,
, This article was processed using the L A T E X macro package with LLNCS style