Filtrer vos résultats
- 52
- 4
- 1
- 22
- 17
- 8
- 4
- 2
- 1
- 1
- 1
- 1
- 11
- 2
- 57
- 2
- 3
- 2
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 5
- 1
- 5
- 2
- 4
- 1
- 2
- 2
- 3
- 2
- 3
- 1
- 1
- 2
- 1
- 1
- 50
- 6
- 1
- 56
- 3
- 3
- 3
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 57
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
57 résultats
|
|
|
triés par
|
|
|
Mathematics and Proof Presentation in PcoqRR-4313, INRIA. 2001
Rapport
inria-00072274v1
|
||
|
|
Links between homotopy theory and type theoryCICM - Conference on Intelligent Computer Mathematics, Jul 2014, Coimbra, Portugal
Communication dans un congrès
hal-00987248v1
|
||
|
|
Formal Verification of a Geometry Algorithm: A Quest for Abstract Views and Symmetry in Coq ProofsICTAC 2018 - International Colloquium on Theoretical of Computing, Oct 2018, Stellenbosch, South Africa
Communication dans un congrès
hal-01866271v1
|
||
|
|
Formalizing Convex Hulls AlgorithmsTPHOLs 2001 - 14th International Conference Theorem Proving in Higher Order Logics, Sep 2001, Edinburgh, United Kingdom. pp.346-361, ⟨10.1007/3-540-44755-5_24⟩
Communication dans un congrès
hal-01702679v1
|
||
|
|
Inductive and Coinductive Components of Corecursive Functions in CoqCoalgebraic Methods in Computer Science, Apr 2008, Budapest, Hungary
Communication dans un congrès
inria-00277075v2
|
||
|
|
A combination of a dynamic geometry software with a proof assistant for interactive formal proofs9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom
Communication dans un congrès
inria-00585400v1
|
||
|
|
Theorem proving support in programming language semantics[Research Report] RR-6242, INRIA. 2007, pp.23
Rapport
inria-00160309v2
|
||
|
|
A Machine-Checked Proof of the Odd Order TheoremITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.163-179, ⟨10.1007/978-3-642-39634-2_14⟩
Communication dans un congrès
hal-00816699v1
|
||
|
|
Affine functions and series with co-inductive real numbersMathematical Structures in Computer Science, 2006, 17 (1), pp.37-63. ⟨10.1017/S0960129506005809⟩
Article dans une revue
inria-00001171v2
|
||
|
|
Implementing Proof by Pointing without a Structure EditorRR-3286, INRIA. 1997
Rapport
inria-00073402v1
|
||
|
|
Real theorem provers deserve real user-interfaces[Research Report] RR-1684, INRIA. 1992
Rapport
inria-00076907v1
|
||
|
|
A Canonical calculus of residuals[Research Report] RR-1542, INRIA. 1991, pp.12
Rapport
inria-00075020v1
|
||
|
|
Programming Language Specifications and Environments[Technical Report] RT-0212, INRIA. 1997, pp.47
Rapport
inria-00069959v1
|
||
|
|
Vérification formelle d'extractions de racines entièresRevue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2005, Langages Applicatifs, Spécifications, Programmation, Vérification, 24 (9), pp.1161-1195
Article dans une revue
inria-00001172v1
|
||
|
|
User Guide to the CTCOQ Proof Environment[Technical Report] RT-0210, INRIA. 1997, pp.63
Rapport
inria-00069961v1
|
||
|
|
Coq in a Hurry3rd cycle. Types Summer School, also used at the University of Goteborg, Nice,
Cours
inria-00001173v6
Ecole Jeunes Chercheurs en Programmation, Universite de Nice, France. 2016, pp.49 |
||
|
|
Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifsJournées Francophones des Langages Applicatifs, INRIA, Jan 2006, Pauillac, pp.41-55
Communication dans un congrès
inria-00000480v1
|
||
|
|
Structural abstract interpretation, A formal study using CoqLERNET Summer School, Ana Bove and Jorge Sousa Pinto, Feb 2008, Piriapolis, Uruguay
Communication dans un congrès
inria-00329572v2
|
||
Interactive theorem proving and program development. Coq'Art: The Calculus of inductive constructions.Springer Verlag, pp.470, 2004, Texts in Theoretical Computer Science
Ouvrages
hal-00344237v1
|
|||
|
|
Views of Pi: definition and computationJournal of Formalized Reasoning, 2014, 7 (1), pp.105-129. ⟨10.6092/issn.1972-5787/4343⟩
Article dans une revue
hal-01074926v1
|
||
|
|
QArith: Coq Formalisation of Lazy Rational Arithmetic[Research Report] RR-5004, INRIA. 2003, pp.19
Rapport
inria-00077041v1
|
||
|
|
A formal study of Bernstein coefficients and polynomialsMathematical Structures in Computer Science, 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩
Article dans une revue
inria-00503017v2
|
||
|
|
Reasoning with Executable SpecificationsRR-2780, INRIA. 1996
Rapport
inria-00073912v1
|
||
|
|
Formal study in Coq of pi computations using arithmetic-geometric meansLogiciel hal-01767263v1 |
||
|
|
lambda-calcul et typesEcole Jeunes Chercheurs en Programmation (CNRS-INRIA) Toulouse, 2006
Cours
inria-00083975v1
|
||
|
|
Prouvez que vos programmes fonctionnels n'ont pas de bugs avec Coq Première partieProgrammez !, 2023, 256, pp.35
Article dans une revue
hal-04219914v1
|
||
|
|
Changements de représentation des données dans le calcul des constructions inductives[Rapport de recherche] RR-4039, INRIA. 2000, pp.29
Rapport
inria-00072599v1
|
||
Homotopy Type Theory: Univalent Foundations of MathematicsThe Univalent Foundations Program Institute for Advanced Study, pp.1--587, 2013
Ouvrages
hal-00935057v1
|
|||
|
|
A structured approach to proving compiler optimizations based on dataflow analysisTypes for Proofs and Programs, Workshop TYPES 2004, Dec 2004, Jouy-en-Josas, France. pp.66-81, ⟨10.1007/11617990⟩
Communication dans un congrès
inria-00289549v1
|
||
|
|
A certified Compiler for an Imperative LanguageRR-3488, INRIA. 1998
Rapport
inria-00073199v1
|
- 1
- 2