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
|
||
|
|
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
|
||
|
|
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
|
||
|
|
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
|
||
|
|
A certified Compiler for an Imperative LanguageRR-3488, INRIA. 1998
Rapport
inria-00073199v1
|
||
|
|
Filters on Co-Inductive streams: an application to Eratosthenes' sieveRR-5343, INRIA. 2004, pp.21
Rapport
inria-00070658v1
|
||
Formal proof of theorems on genetic regulatory networksSYNASC'09, Sep 2009, Timisoara, Romania
Communication dans un congrès
inria-00504065v1
|
|||
|
|
Semantics for programming languages with Coq encodingsMaster. France. 2015
Cours
cel-01130272v1
|
||
|
|
Fixed Precision Patterns for the Formal Verification of Mathematical Constant ApproximationsCertified Programs and Proofs (CPP'15), Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693172⟩
Communication dans un congrès
hal-01074927v1
|
||
|
|
Formal Proofs of Transcendence for e and π as an Application of Multivariate and Symmetric PolynomialsCertified Programs and Proofs, Jan 2016, St Petersburg, Florida, United States. pp.12
Communication dans un congrès
hal-01240025v1
|
||
|
|
Reasoning with Executable SpecificationsRR-2780, INRIA. 1996
Rapport
inria-00073912v1
|
||
|
|
Formal study in Coq of pi computations using arithmetic-geometric meansLogiciel hal-01767263v1 |
- 1
- 2