|
|
A Tactic Language for the System Coq
David Delahaye
Proceedings of Logic for Programming and Automated Reasoning (LPAR), Jan 2000, Réunion, France. pp.85-95
Communication dans un congrès
hal-01125070v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Confluence and Preservation of Strong Normalisation in an Explicit Substitutions Calculus
César Augusto Munoz Hurtado
[Research Report] RR-2762, INRIA. 1995
Rapport
inria-00073929v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Proof Normalization Modulo
Gilles Dowek
,
Benjamin Werner
[Research Report] RR-3542, INRIA. 1998
Rapport
inria-00073143v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Proof of Weak Termination of the Simply-Typed {$\lambda\sigma$}-Calculus
Jean Goubault-Larrecq
[Research Report] RR-3090, INRIA. 1997
Rapport
inria-00073601v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Lambda-Calculus, Combinators and the Comprehension Scheme
Gilles Dowek
[Research Report] RR-2565, INRIA. 1995
Rapport
inria-00074116v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
The Coq Proof Assistant : A Tutorial : Version 7.2
Gérard Huet
,
Gilles Kahn
,
Christine Paulin-Mohring
[Research Report] RT-0256, INRIA. 2002, pp.46
Rapport
inria-00069918v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
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
Hugo Herbelin
Informatique [cs]. Université Paris-Diderot - Paris VII, 1995. Français. ⟨NNT : ⟩
Thèse
tel-00382528v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Search2: un outil de recherche dans une bibliothèque de preuves Coq modulo isomorphismes
David Delahaye
[Research Report] CEDRIC-97-730, CEDRIC Lab/CNAM. 1997
Rapport
hal-01124981v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Games and Weak-Head Reduction for Classical PCF
Hugo Herbelin
Communication dans un congrès
inria-00381542v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Le Sens du calcul
Gilles Dowek
1996
Pré-publication, Document de travail
hal-04044989v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Collections, Sets and Types
Gilles Dowek
[Research Report] RR-2708, INRIA. 1995
Rapport
inria-00073982v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Few Remarks on SKInT
Jean Goubault-Larrecq
[Research Report] RR-3475, INRIA. 1998
Rapport
inria-00073214v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
The Coq Proof Assistant, Reference Manual, Version 5.10
Cristina Cornes
,
Judicaël Courant
,
Jean-Christophe Filliâtre
,
Gérard Huet
,
Pascal Manoury
,
et al.
[Research Report] RT-0177, INRIA. 1995, pp.185
Rapport
inria-00069994v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
The Coq Proof Assistant Reference Manual : Version 6.1
Bruno Barras
,
Samuel Boutin
,
Cristina Cornes
,
Judicaël Courant
,
Jean-Christophe Filliâtre
,
et al.
[Research Report] RT-0203, INRIA. 1997, pp.214
Rapport
inria-00069968v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory
César Muñoz
[Research Report] RR-3309, INRIA. 1997
Rapport
inria-00073380v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Meta-Theoretical Properties of lambda_phi: A Left-Linear Variant of lambda_sigma
César Muñoz
[Research Report] RR-3107, INRIA. 1997
Rapport
inria-00073584v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Proving Correctness of the Translation from Mini-ML to the CAM with the Coq Proof Development System
Samuel Boutin
[Research Report] RR-2536, INRIA. 1995
Rapport
inria-00074142v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Axiomatisation d'un Lambda-Calcul avec Substitutions Explicites dans Coq
Amokrane Saibi
[Rapport de recherche] RR-2345, INRIA. 1994
Rapport
inria-00074332v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Une Théorie des Constructions Inductives
Benjamin Werner
Génie logiciel [cs.SE]. Université Paris-Diderot - Paris VII, 1994. Français. ⟨NNT : ⟩
Thèse
tel-00196524v2
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Generic Normalisation Proof for Pure Type Systems
Paul-André Melliès
,
Benjamin Werner
[Research Report] RR-3548, INRIA. 1998
Rapport
inria-00073135v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Proof Normalization for a First-order Formulation of Higher-order Logic
Gilles Dowek
[Research Report] RR-3383, INRIA. 1998
Rapport
inria-00073306v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Type-Free Formalization of Mathematics where Proofs are Objects
Gilles Dowek
[Research Report] RR-2915, INRIA. 1996
Rapport
inria-00073782v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction
Jean Goubault-Larrecq
[Research Report] RR-3653, INRIA. 1999
Rapport
inria-00073019v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
La part du calcul
Gilles Dowek
Computer Science [cs]. Université de Paris 7, 1999
HDR
tel-04114581v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
A Tutorial on Recursive Types in Coq
Eduardo Giménez
[Research Report] RT-0221, INRIA. 1998, pp.42
Rapport
inria-00069950v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Order-theoretic, geometric and combinatorial models of intuitionistic S4 proofs
Jean Goubault-Larrecq
,
Eric Goubault
IMLA 1999 - 1st Workshop on Intuitionistic Modal Logics and Applications, Jul 1999, Trento, Italy
Communication dans un congrès
hal-03208846v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
The Coq Proof Assistant : A Tutorial : Version 6.1
Gérard Huet
,
Gilles Kahn
,
Christine Paulin-Mohring
[Research Report] RT-0204, INRIA. 1997, pp.44
Rapport
inria-00069967v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Reflecting BDDs in Coq
Kumar Neeraj Verma
,
Jean Goubault-Larrecq
[Research Report] RR-3859, INRIA. 2000
Rapport
inria-00072797v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
The Three Gap Theorem : Specification and Proof in Coq
Micaela Mayero
[Research Report] RR-3848, INRIA. 1999
Rapport
inria-00072808v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|
|
|
Coq en Coq
Bruno Barras
[Research Report] RR-3026, INRIA. 1996
Rapport
inria-00073667v1
|
Partager
Gmail
Facebook
X
LinkedIn
More
|