Sites Inria

English version

Equipe de recherche COQ

Publications de l'équipe COQ

2004

Autre publication

titre
A Tutorial on [Co-]Inductive types in Coq
auteur
Pierre Castéran, Eduardo Gimenez
article
2004
Accès au bibtex
BibTex

2002

Rapport

titre
The Coq Proof Assistant : A Tutorial : Version 7.2
auteur
Gérard Huet, Gilles Kahn, Christine Paulin-Mohring
article
[Research Report] RT-0256, INRIA. 2002, pp.46
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069918/file/RT-0256.pdf BibTex

2000

Communication dans un congrès

titre
The duality of computation
auteur
Hugo Herbelin, Pierre-Louis Curien
article
Fifth ACM SIGPLAN International Conference on Functional Programming : ICFP '00, Sep 2000, Montréal, Canada. pp.233-243
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00156377/file/icfp-CuHer00-duality_errata.pdf BibTex
titre
A Tactic Language for the System Coq
auteur
David Delahaye
article
Proceedings of Logic for Programming and Automated Reasoning (LPAR), Jan 2000, Réunion, France. pp.85-95
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01125070/file/ltac%20%28LPAR%2700%29.pdf BibTex

Rapport

titre
Reflecting BDDs in Coq
auteur
Kumar Neeraj Verma, Jean Goubault-Larrecq
article
[Research Report] RR-3859, INRIA. 2000
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072797/file/RR-3859.pdf BibTex

1999

Rapport

titre
The Three Gap Theorem : Specification and Proof in Coq
auteur
Micaela Mayero
article
[Research Report] RR-3848, INRIA. 1999
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072808/file/RR-3848.pdf BibTex
titre
A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction
auteur
Jean Goubault-Larrecq
article
[Research Report] RR-3653, INRIA. 1999
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073019/file/RR-3653.pdf BibTex

1998

Rapport

titre
A Tutorial on Recursive Types in Coq
auteur
Eduardo Giménez
article
[Research Report] RT-0221, INRIA. 1998, pp.42
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069950/file/RT-0221.pdf BibTex
titre
A Few Remarks on SKInT
auteur
Jean Goubault-Larrecq
article
[Research Report] RR-3475, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073214/file/RR-3475.pdf BibTex
titre
A Generic Normalisation Proof for Pure Type Systems
auteur
Paul-André Melliès, Benjamin Werner
article
[Research Report] RR-3548, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073135/file/RR-3548.pdf BibTex
titre
Proof Normalization Modulo
auteur
Gilles Dowek, Benjamin Werner
article
[Research Report] RR-3542, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073143/file/RR-3542.pdf BibTex
titre
Proof Normalization for a First-order Formulation of Higher-order Logic
auteur
Gilles Dowek
article
[Research Report] RR-3383, INRIA. 1998
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073306/file/RR-3383.pdf BibTex

1997

Communication dans un congrès

titre
Games and Weak-Head Reduction for Classical PCF
auteur
Hugo Herbelin
article
Typed Lambda Calculi and Applications 1997, Apr 1997, Nancy, France. pp.214--230, ⟨10.1007/3-540-62688-3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00381542/file/tlca-Her97-classical-games.pdf BibTex

Rapport

titre
The Coq Proof Assistant : A Tutorial : Version 6.1
auteur
Gérard Huet, Gilles Kahn, Christine Paulin-Mohring
article
[Research Report] RT-0204, INRIA. 1997, pp.44
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069967/file/RT-0204.pdf BibTex
titre
The Coq Proof Assistant Reference Manual : Version 6.1
auteur
Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saïbi, Benjamin Werner
article
[Research Report] RT-0203, INRIA. 1997, pp.214
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069968/file/RT-0203.pdf BibTex
titre
A Proof of Weak Termination of the Simply-Typed {$\lambda\sigma$}-Calculus
auteur
Jean Goubault-Larrecq
article
[Research Report] RR-3090, INRIA. 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073601/file/RR-3090.pdf BibTex
titre
On Computational Interpretations of the Modal Logic S4 IIIb. Confluence, Termination of the $\lambda\mbox{ev}Q_H$-Calculus
auteur
Jean Goubault-Larrecq
article
[Research Report] RR-3164, INRIA. 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073524/file/RR-3164.pdf BibTex
titre
Meta-Theoretical Properties of lambda_phi: A Left-Linear Variant of lambda_sigma
auteur
César Muñoz
article
[Research Report] RR-3107, INRIA. 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073584/file/RR-3107.pdf BibTex
titre
A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory
auteur
César Muñoz
article
[Research Report] RR-3309, INRIA. 1997
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073380/file/RR-3309.pdf BibTex
titre
Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes
auteur
David Delahaye
article
[Research Report] CEDRIC-97-730, CEDRIC Lab/CNAM. 1997
Accès au bibtex
BibTex

1996

Rapport

titre
Coq en Coq
auteur
Bruno Barras
article
[Research Report] RR-3026, INRIA. 1996
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073667/file/RR-3026.pdf BibTex
titre
A Type-Free Formalization of Mathematics where Proofs are Objects
auteur
Gilles Dowek
article
[Research Report] RR-2915, INRIA. 1996
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073782/file/RR-2915.pdf BibTex

1995

Rapport

titre
Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System
auteur
Samuel Boutin
article
[Research Report] RR-2536, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074142/file/RR-2536.pdf BibTex
titre
Lambda-Calculus, Combinators and the Comprehension Scheme
auteur
Gilles Dowek
article
[Research Report] RR-2565, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074116/file/RR-2565.pdf BibTex
titre
The Coq Proof Assistant, Reference Manual, Version 5.10
auteur
Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Pascal Manoury, César Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, Benjamin Werner
article
[Research Report] RT-0177, INRIA. 1995, pp.185
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00069994/file/RT-0177.pdf BibTex
titre
Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus
auteur
César Augusto Munoz Hurtado
article
[Research Report] RR-2762, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073929/file/RR-2762.pdf BibTex
titre
Collections, Sets and Types
auteur
Gilles Dowek
article
[Research Report] RR-2708, INRIA. 1995
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073982/file/RR-2708.pdf BibTex

Thèse

titre
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
auteur
Hugo Herbelin
article
Informatique [cs]. Université Paris-Diderot - Paris VII, 1995. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00382528/file/These-Her95.pdf BibTex

1994

Communication dans un congrès

titre
A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure
auteur
Hugo Herbelin
article
Computer Science Logic, Sep 1994, Kazimierz, Poland. pp.61--75
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00381525/file/csl-Her94-lambda-bar.pdf BibTex

Rapport

titre
Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq
auteur
Amokrane Saibi
article
[Rapport de recherche] RR-2345, INRIA. 1994
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00074332/file/RR-2345.pdf BibTex

Thèse

titre
Une Théorie des Constructions Inductives
auteur
Benjamin Werner
article
Génie logiciel [cs.SE]. Université Paris-Diderot - Paris VII, 1994. Français
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00196524/file/main.pdf BibTex

Suivez Inria