| [5] |
J. Courant,,
1997. À paraître,Rapport de Recherche INRIA 2915, 1996.
Un calcul de modules pour les systèmes de types purs,
thèse de doctorat, Ecole Normale Supérieure de Lyon, 1998.
BibTeX entry |
| [6] |
E. Giménez,
Un Calcul de Constructions Infinies et son application a la
vérification de systèmes communicants,
thèse d'université, Ecole Normale Supérieure de Lyon,
décembre 1996.
BibTeX entry |
| [7] |
H. Herbelin,
Séquents qu'on calcule : de l'interprétation du calcul des
séquents comme calcul de lambda-termes et comme calcul de stratégies
gagnantes,
Thèse d'université, Université Paris 7, Janvier 1995.
BibTeX entry |
| [8] |
C. Muñoz,
Un calcul de substitutions pour la représentation de preuves
partielles en théorie de types,
thèse de doctorat, Paris 7, novembre 1997.
BibTeX entry |
| [9] |
C. Parent,
Synthèse de preuves de programmes dans le Calcul des
Constructions Inductives,
thèse d'université, École Normale Supérieure de Lyon, janvier 1995.
BibTeX entry |
| [10] |
C. Paulin-Mohring,
Définitions Inductives en Théorie des Types d'Ordre
Supérieur,
Habilitation à diriger les recherches, Université Claude Bernard Lyon
I, décembre 1996.
BibTeX entry |
|
[11] |
A. Saïbi,
Algèbre Constructive en Théorie des Types, Outils génériques
pour la modélisation et la démonstration, Application à la théorie des
Catégories,
thèse de doctorat, Université Paris VI, 1998.
BibTeX entry |
| [12] |
V. Ménissier-Morain,
Arithmétique exacte. Conception, algorithmique et performances
d'une implémentation informatique en précision arbitraire,
thèse de doctorat, Université Paris VII, Déc. 1994.
BibTeX entry |
| [13] |
B. Werner,
Une Théorie des Constructions Inductives,
thèse de doctorat, Université Paris VII, Mai. 1994.
BibTeX entry |
| [14] |
S. Boutin,
Réflexions sur les quotients,
thèse d'université, Paris 7, avril 1997.
BibTeX entry |
| [15] |
C. Cornes,
Conception d'un Langage de Haut Niveau de Représentation de
Preuves: récurrence par filtrage de motifs, unification en présence de types
inductifs primitifs. synthèse de lemmes d'inversion,
Thèse d'université, Paris 7, novembre 1997.
BibTeX entry, PS |
| [16] |
T. Coquand, H. Herbelin,
``A-translation and Looping Combinators in Type Systems'',
Journal of Functional Programming 4, 1994, p. 77-88.
BibTeX entry |
| [17] |
G. Dowek,
``Third order matching is decidable'',
Annals of Pure and Applied Logic, 69, pp. 135-155, 1994.
BibTeX entry |
| [18] |
G. Dowek,
``Collections, sets and types'',
Mathematical Structures in Computer Science, 1998,
A paraître.
BibTeX entry |
| [19] |
G. Dowek,
Handbook of Automated Reasoning,
Elsevier, 1997, ch. Higher-order unification and matching,
À paraître.
BibTeX entry |
| [20] |
H. Herbelin,
``ESPRIT Basic Research Action 6453, TYPES: Types for Proofs
and Programs'',
Bulletin of the European Association for Theoretical Computer
Science, 1994.
BibTeX entry |
| [21] |
G. Huet,
``An analysis of Böhm's theorem'',
in: To C. Böhm: Essays on Lambda-Calculus and Functional
Programming, S. R. d. R. M. Dezani-Ciancaglini et M. V. Zilli (réd.),
Cambridge University Press, 1993.
BibTeX entry |
| [22] |
G. Huet,
``Residual theory in lambda-calculus: a formal
development'',
Journal of Functional Programming 4,3, 1994, p. 371-394.
BibTeX entry |
| [23] |
G. Huet,
``The Zipper Data Structure'',
Journal of Functional Programming, 1997,
à paraitre.
BibTeX entry |
| [24] |
G. Huet,
``Regular Böhm Trees'',
Math. Struct. in Comp. Science, à paraître 1998.
BibTeX entry |
| [25] |
G. Huet, A. Saïbi,
Constructive Category Theory,
MIT Press, à paraitre 1998,
version préliminaire présentée au CLICS-TYPES BRA meeting, 95.
BibTeX entry |
| [26] |
C. Parent,
``Verifying programs in the Calculus of Inductive
Constructions'',
Formal Aspects of Computing, 1997,
A paraître.
BibTeX entry |
| [27] |
B. Barras,
``Verification of the Interface of a Small Proof System in Coq'',
in: Workshop on Types for Proofs and Programs (TYPES'96),
1997. À paraître.
BibTeX entry |
| [28] |
S. Boutin,
``Using reflection to build efficient and certified decision
procedures'',
in: TACS'97, M. Abadi, T. Ito (réd.), 1281, LNCS,
Springer-Verlag,
1997.
BibTeX entry |
| [29] |
C. Cornes, D. Terrasse,
``Inverting Inductive Predicates in Coq'',
in: BRA Workshop on Types for Proofs and Programs
(TYPES'95), LNCS, 1158,
1996.
BibTeX entry, PS |
| [30] |
J. Courant,
``An applicative module calculus'',
in: TAPSOFT'97, LNCS, Springer-Verlag,
Lille, France, avril 1997.
BibTeX entry, DVI, PS |
| [31] |
J. Courant,
``A Module Calculus for Pure Type Systems'',
in: TLCA'97, LNCS, Springer-Verlag, p. 112 -
128,
1997.
BibTeX entry, DVI, PS |
| [32] |
P.-L. Curien, H. Herbelin,
``Computing with Abstract Böhm Trees'',
Kyoto, Japan, Mars 1998. to appear in the proceedings of the FUJI
Symposium on Functional and Logic Programming.
BibTeX entry |
| [33] |
V. Danos, H. Herbelin, L. Regnier,
``Game Semantics and Abstract Machines'',
in: Proceedings, Eleventh Annual IEEE Symposium on Logic in
Computer Science, IEEE Computer Society Press,
New Brunswick, New Jersey, July 1996.
BibTeX entry |
| [34] |
F. Damiani, F. Prost,
``Detecting and Removing Dead Code using Rank 2
Intersection'',
in: Proceedings TYPES'96, E. Giménez, C. Paulin-Mohring
(réd.),
mai 1997. À paraître, rapport de recherche LIP, ENS Lyon RR97-10).
BibTeX entry |
|
[35] |
D. Delahaye, R. di Cosmo, B. Werner,
``Recherche dans une bibliothèque de preuves Coq en
utilisant le type et modulo isomorphismes'',
in: PRC/GDR de programmation, Pôle Preuves et Spécifications
Algébriques,
novembre 1997.
BibTeX entry |
| [36] |
G. Dowek,
``Automated theorem proving in type theory, course
notes'',
in: Second international summer school in logic for computer
science, Chambéry France, M. Parigot (réd.),
1994.
BibTeX entry |
| [37] |
G. Dowek,
``Lambda-calculus, combinators and the comprehension
scheme'',
in: Typed Lambda Calculi and Applications, p. 154-170,
1995. Rapport de Recherche INRIA 2565, 1995.
BibTeX entry |
| [38] |
G. Dowek,
``Collections, sets and types. (abstract)'',
in: Logic, Methodology and Philosophy of Science, p. 402,
1995. Rapport de Recherche INRIA 2708, 1995.
BibTeX entry |
| [39] |
G. Dowek,
``Proof normalization for a first-order formulation of
higher-order logic'',
in: Proceedings of Theorem proving in higher order logics,
Lecture Notes in Computer Science, 1275, p. 105-119,
1997.
BibTeX entry |
| [40] |
G. Dowek,
``A type-Free formalization of mathematics where proofs are
objects'',
in: ,
1997. À paraître,Rapport de Recherche INRIA 2915, 1996.
BibTeX entry |
| [41] |
G. Dowek,
``Le langage mathématique et les langages de
programmation'',
in: Voir, entendre, raisonner, calculer,
1997.
BibTeX entry |
| [42] |
G. Dowek, T. Hardin, C. Kirchner,
``Higher-order unification via explicit
substitutions'',
in: Logic in Computer Science, p. 366-374,
1995.
BibTeX entry |
| [43] |
G. Dowek, T. Hardin, C. Kirchner,
F. Pfenning,
``Higher-order unification via explicit substitutions: the
case of higher-order patterns'',
in: Joint international conference and symposium on logic
programming, p. 259-273,
1996.
BibTeX entry |
| [44] |
E. Giménez,
``Codifying guarded definitions with recursive
schemes'',
in: BRA Workshop on Types for Proofs and Programs
(TYPES'94), LNCS 996, p. 39-59,
1994.
BibTeX entry |
| [45] |
E. Giménez,
``An application of co-Inductive types in Coq: verification
of the Alternating Bit Protocol'',
in: BRA Workshop on Types for Proofs and Programs
(TYPES'95), LNCS, 1158,
1996.
BibTeX entry |
| [46] |
H. Geuvers, B. Werner,
``On the Church-Rosser Property for Expressive Type Systems
and its Consequences for their Metatheoretic Study'',
in: Proceedings of LICS 94, Paris, France, S. Abramsky
(réd.),
1994.
BibTeX entry |
| [47] |
H. Herbelin,
``A lambda-calculus structure isomorphic to sequent
calculus structure'',
in: Computer Science Logic, Lecture Notes in Computer
Science, 933, Springer-Verlag,
1995.
BibTeX entry |
| [48] |
H. Herbelin,
``Games and Weak Head Reduction for Lambda-Calculus +
Catch'',
in: Proceedings of Typed Lambda Calculi and Applications,
1997, P. de Groote et J. R. Hindley (réd.), LNCS, 1210,
Springer-Verlag,
Nancy, France, April 1997.
BibTeX entry |
| [49] |
G. Huet, H. Laulhère,
``Finite-state Transducers as Regular Böhm Trees'',
in: Theoretical Aspects of Computer Software, M. Abadi,
T. Ito (réd.), Lecture Notes in Computer Science, 1281,
Springer-Verlag, p. 604-610,
septembre 1997.
BibTeX entry |
| [50] |
J. Goubault-Larrecq,
``Clap, a Simple Language for Cryptographic
Protocols'', 1997. à paraître.
BibTeX entry, PS |
| [51] |
J. Goubault-Larrecq,
``Ramified Higher-Order Unification'',
in: 12th Annual IEEE Symposium on Logics in Computer Science
(LICS'97),
Varsovie, Pologne, juillet 1997.
BibTeX entry, PS |
| [52] |
F. Leclerc, C. Paulin-Mohring,
``Programming with Streams in Coq. A case study: the Sieve
of Eratosthenes'',
in: Proceedings of Types'93, H. Barendregt, T. Nipkow
(réd.),
1994.
BibTeX entry |
| [53] |
F. Prost,
``ML Type Inference for Dead Code Analysis'',
in: Proceedings TYPES'96, E. Giménez, C. Paulin-Mohring
(réd.),
1997. À paraître.
BibTeX entry |
| [54] |
P.-A. Melliès, B. Werner,
``A Generic Normalization Proof for Pure Type
Systems'',
in: TYPES'96, C. Paulin-Mohring, E. Gimenez (réd.), LNCS,
Springer-Verlag,
1997.
BibTeX entry |
|
[55] |
C. Muñoz,
``Confluence and Preservation of Strong Normalisation in an
Explicit Substitutions Calculus (Extended Abstract)'',
in: Proceedings, Eleventh Annual IEEE Symposium on Logic in
Computer Science, IEEE Computer Society Press,
New Brunswick, New Jersey, juillet 1996.
BibTeX entry, PS |
| [56] |
C. Muñoz,
``Proof Representation in Type Theory: State of the
Art'',
in: Proceedings, XXII Latinamerican Conference of Informatics
CLEI Panel 96,
Santafé de Bogotá, Colombia, juin 1996.
BibTeX entry |
| [57] |
C. Muñoz,
``A Left-linear Variant of lambdasigma'',
in: Proceedings of the International Conference
PLILP/ALP/HOA'97, LNCS, 1298, Springer,
Southampton (England), September 1997.
BibTeX entry, PS |
| [58] |
C. Muñoz,
``Dependent Types with Explicit Substitutions: A
meta-theoretical development'',
in: Types for Proofs and Programs, Proceedings of
International Workshop TYPES'96,
1997.
BibTeX entry, PS |
| [59] |
P. H. Schmitt, J. Goubault-Larrecq,
``A Tableau System for Linear-TIME Temporal Logic'',
in: 3rd International Workshop on Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'97), Springer Verlag,
Université de Twente, Enschede, Pays-Bas, avril 1997.
BibTeX entry, PS |
|
[60] |
C. Parent,
``Developing certified programs in the system Coq - The
Program tactic'',
in: Proceedings of Types'93, H. Barendregt, T. Nipkow
(réd.),
1994. également rapport LIP-ENS Lyon RR 93-29 and by anonymous ftp
from lip.ens-lyon.fr file pub/Rapports/RR/RR93/RR93-29.ps.Z.
BibTeX entry |
| [61] |
C. Parent,
``Synthesizing proofs from programs in the Calculus of
Inductive Constructions'',
in: Third International Conference on the Mathematics of
Program Construction, Lecture Notes in Computer Science, 947,
Springer-Verlag,
Juillet 1995.
BibTeX entry |
| [62] |
C. Parent,
``Natural proofs versus programs optimization in the Calculus
of Inductive Constructions'',
in: Theorem Proving in Higher-Order Logic,
1996. Poster Session.
BibTeX entry |
|
[63] |
C. Paulin-Mohring,
``Circuits as streams in Coq : Verification of a sequential
multiplier'',
in: Types for Proofs and Programs (TYPES'95), S. Berardi,
M. Coppo (réd.), LNCS, 1158,
1996. également Rapport de Recherche LIP 95-16.
BibTeX entry |
| [64] |
A. Saïbi,
``Typing algorithm in type theory with inheritance'',
in: Proceedings of The 24th Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, ACM Press,
Paris, France, janvier 1997.
BibTeX entry |
| [65] |
B. Werner,
``Sets in Types, Types in Sets'',
in: TACS'97, M. Abadi, T. Ito (réd.), 1281, LNCS,
Springer-Verlag,
1997.
BibTeX entry |
| [66] |
C. Cornes,
``Compilation du Filtrage de Motifs avec Types Dépendants
dans le Système Coq'',
in: Actes des Journées du GDR Programmation 1996,
Orleans, France, Novembre 1996.
BibTeX entry |
| [67] |
P. Audebaud,
``Explicit substitutions for the lambda-mu calculus'',
rapport de recherche No94-26, LIP ENS-Lyon, 1994.
BibTeX entry |
| [68] |
C. Barraband,
Etude du principe d'induction généralisée pour les types de
données inductifs,
Mémoire du DEA d'informatique fondamentale, Université Paris 7,
septembre 1994.
BibTeX entry |
|
[69] |
B. Barras,
Coq en Coq,
Mémoire du DEA informatique, mathématiques et applications, École
Polytechnique, 1995,
Rapport de recherche INRIA 3026, octobre 1996.
BibTeX entry |
| [70] |
B. Barras, B. Werner,
``Coq in Coq'',
Soumis, 1997.
BibTeX entry, PS |
| [71] |
J.-R. Beauvais,
Une logique du premier ordre exprimant le bon typage des
propositions,
Mémoire du DEA informatique fondamentale, Paris 7, 1995.
BibTeX entry |
| [72] |
S. Boutin,
``Proving Correctness of the translation from Mini-ML to the
CAM with the Coq Proof Development System'',
rapport de recherche No2536, INRIA, avril 1995.
BibTeX entry |
| [73] |
C. Cornes, J. Courant, J.-C. Filliâtre, G. Huet,
P. Manoury, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring,
A. Saïbi, B. Werner,
``The Coq Proof Assistant Reference Manual, Version
5.10'',
rapport technique No177, INRIA, juillet 1995.
BibTeX entry |
| [74] |
B. Barras, S. Boutin, C. Cornes, J. Courant,
J. Filliatre, E. Giménez, H. Herbelin, G. Huet, C. M. noz, C. Murthy,
C. Parent, C. Paulin, A. Saïbi, B. Werner,
``The Coq Proof Assistant Reference Manual - Version
V6.1'',
rapport de recherche No0203, INRIA, août 1997.
BibTeX entry |
|
[75] |
G. Huet, G. Kahn, C. Paulin-Mohring,
``The Coq Proof Assistant - A tutorial'',
rapport technique No178, INRIA, Juillet 1995,
Version révisée distribuée avec Coq.
BibTeX entry |
| [76] |
G. Huet, G. Kahn, C. Paulin-Mohring,
``The Coq Proof Assistant - A tutorial, Version
6.1'',
rapport technique No204, INRIA, Août 1997,
Version révisée distribuée avec Coq.
BibTeX entry |
| [77] |
J. Courant,
Explicitation de preuves par récurrence implicite,
Mémoire du DEA d'informatique, ENS Lyon, septembre 1994.
BibTeX entry |
|
[78] |
D. Delahaye,
Search1: un outil de recherche dans une bibliothèque de preuves
Coq modulo isomorphismes,
Rapport du DEA sémantique, preuves et programmation, Université
Paris 6, 1997.
BibTeX entry |
| [79] |
G. Dowek, G. Huet, B. Werner,
``On the Definition of the Eta-long Normal Form in Type
Systems of the Cube'',
Soumis à publication, 1997.
BibTeX entry |
| [80] |
J.-C. Filliâtre,
Une procédure de décision pour le Calcul des Prédicats Direct.
Etude et implémentation dans le système Coq,
Mémoire du DEA d'informatique, ENS Lyon, septembre 1994.
BibTeX entry |
| [81] |
J.-C. Filliâtre,
``A decision procedure for Direct Predicate Calculus:
study and implementation in the system Coq'',
rapport de recherche No96-25, LIP - ENS Lyon, 1996.
BibTeX entry |
| [82] |
J.-C. Filliâtre,
``Finite Automata Theory in Coq: A constructive proof of
Kleene's theorem'',
Research Report No97-04, LIP - ENS Lyon, February 1997.
BibTeX entry, PS |
| [83] |
J.-C. Filliâtre,
``Proof of Imperative Programs in Type Theory'',
Research Report No97-24, LIP - ENS Lyon, July 1997.
BibTeX entry, PS |
| [84] |
D. Hirschkoff,
Ecriture d'une tactique arithmétique pour le système Coq,
Mémoire du DEA iarfa, Ecole des Ponts et Chaussées, Paris,
septembre 1994.
BibTeX entry |
| [85] |
G. Huet,
``Certification du logiciel: Méthodes et outils. Etat de l'art
des méthodes formelles en génie logiciel'',
rapport de recherche No11/SGDN/STS/VST, SGDN, April 1994.
BibTeX entry |
| [86] |
J. Goubault-Larrecq,
``On Computational Interpretations of the Modal Logic S4
IIIb. Confluence, Termination of lambdaevQ_H'',
Prépublication (rapport de recherche) NoRR-3164, INRIA,
Projet Coq, Rocquencourt, France, mai 1997.
BibTeX entry, PS |
| [87] |
J. Goubault-Larrecq,
``A Proof of Weak Termination of the Simply-Typed
lambdasigma-Calculus'',
Rapport de recherche No3090, I.N.R.I.A., Projet Coq,
Rocquencourt, France, janvier 1997,
A paraître dans les actes de TYPES'96, Springer Verlag.
BibTeX entry, PS |
| [88] |
D. Larchey-Wendling,
Quelques aspects du polymorphisme paramétrique,
Mémoire du DEA de mathématiques pures, Université Claude Bernard,
Lyon I, septembre 1995.
BibTeX entry |
| [89] |
H. Laulhère,
Axiomatisation des nombres deux-adiques en Coq,
Mémoire du DEA informatique, mathématiques et application, École
Polytechnique, septembre 1995.
BibTeX entry |
| [90] |
P. Loiseleur,
Formalisation en Coq de la norme IEEE 754 sur l'arithmétique
à virgule flottante,
Mémoire, LIP, ENS Lyon, 1997.
BibTeX entry |
| [91] |
M. Mayero,
Le théorème des trois intervalles: spécification et preuves en
Coq,
Rapport du DEA sémantique preuves et programmation, Université
Paris 6, 1997.
BibTeX entry |
|
[92] |
C. Muñoz,
Démonstration automatique dans la logique propositionnelle
intuitionniste,
Mémoire du DEA d'informatique fondamentale, Université Paris 7,
septembre 1994.
BibTeX entry |
| [93] |
C. Muñoz,
``Confluence and Preservation of Strong Normalisation in an
Explicit Substitutions Calculus'',
rapport de recherche NoRR-2762, Unité de recherche
INRIA-Rocquencourt, décembre 1995.
BibTeX entry |
| [94] |
C. Muñoz,
``Meta-Theoretical Properties of lambda_phi: A Left-Linear
Variant of lambdasigma'',
rapport de recherche NoRR-3107, Unité de recherche
INRIA-Rocquencourt, Février 1997.
BibTeX entry |
| [95] |
C. Muñoz,
``A Calculus of Substitutions for Incomplete-Proof
Representation in Type Theory'',
rapport de recherche NoRR-3309, Unité de recherche
INRIA-Rocquencourt, novembre 1997.
BibTeX entry |
| [96] |
S. Philipakis,
Une axiomatisation de logique temporelle en Coq. Étude de cas
avec TLA,
Mémoire de dea, DEA d'Informatique, Nancy I, 1995.
BibTeX entry |
| [97] |
F. Prost,
Optimisation et Logique,
Mémoire du DEA d'informatique fondamentale, ENS Lyon, juin 1995.
BibTeX entry |
| [98] |
F. Prost,
``Marking Techniques for Extraction'',
rapport de recherche No95-47, Laboratoire de
l'Informatique du Parallélisme, ENS Lyon, décembre 1995.
BibTeX entry |
| [99] |
A. Saïbi,
``Axiomatization of a lambda-calculus with
explicit-substitutions in the Coq System'',
rapport de recherche No2345, INRIA, Dec 1994.
BibTeX entry |
|
[100] |
H. Saidi,
Unification dans le système T,
Mémoire du DEA d'informatique fondamentale, Université Paris 7,
Septembre 1994.
BibTeX entry |
| [101] |
B. Werner,
``Diaconescu Constructions in Type Theory'',
rapport de recherche, INRIA, 1998,
à paraître.
BibTeX entry |
| [102] |
A. Chander,
``Secure Mobile Code with Prooflets'',
Rapport de stage, version préliminaire, 1997.
BibTeX entry |
