Recherche - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu

Filtrer vos résultats

225 résultats
keyword_s : Coq
Page :
triés par
Image document

A PCC Architecture based on Certified Abstract Interpretation

 Frédéric Besson , Thomas Jensen , David Pichardie
[Research Report] PI 1764, 2005, pp.35
Rapport inria-00000866v1

Certification of Termination Proofs Using Polynomial Interpretations

 Sébastien Hinderer
17th European Summer School in Logic, Language and Information - ESSLLI '05, Aug 2005, Edimbourg/Grande Bretagne
Communication dans un congrès inria-00001205v1
Image document

Some Formal Tools for Computer Arithmetic: Flocq and Gappa

 Sylvie Boldo , Guillaume Melquiond
ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy
Communication dans un congrès hal-03233227v1
Image document

Bibliothèque certifiée en Coq pour la provenance des données

 Rébecca Zucchini
Logique en informatique [cs.LO]. Université Paris-Saclay, 2023. Français. ⟨NNT : 2023UPASG040⟩
Thèse tel-04165484v1
Image document

Safe reconfiguration of Coqcots and Pycots components

 Jérémy Buisson , Fabien Dagnat , Elena Leroux , Sébastien Martinez
Journal of Systems and Software, 2016, 122, pp.430-444. ⟨10.1016/j.jss.2015.11.039⟩
Article dans une revue hal-01235602v1
Image document

A simple test qualifying the accuracy of Horner's rule for polynomials

 Sylvie Boldo , Marc Daumas
[Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p
Rapport hal-02102015v1
Image document

Formal Foundations of 3D Geometry to Model Robot Manipulators

 Reynald Affeldt , Cyril Cohen
Conference on Certified Programs and Proofs 2017, Jan 2017, Paris, France
Communication dans un congrès hal-01414753v1
Image document

Measure Construction by Extension in Dependent Type Theory with Application to Integration

 Reynald Affeldt , Cyril Cohen
Journal of Automated Reasoning, 2023, 67 (3), pp.28. ⟨10.1007/s10817-023-09671-5⟩
Article dans une revue hal-04183173v1
Image document

Views of Pi: definition and computation

 Yves Bertot , Guillaume Allais
Journal of Formalized Reasoning, 2014, 7 (1), pp.105-129. ⟨10.6092/issn.1972-5787/4343⟩
Article dans une revue hal-01074926v1
Image document

Kleene Algebra with Tests and Coq Tools for While Programs

 Damien Pous
Interactive Theorem Proving 2013, Jul 2013, Rennes, France. pp.180-196, ⟨10.1007/978-3-642-39634-2_15⟩
Communication dans un congrès hal-00785969v1
Image document

HOCore in Coq

 Petar Maksimovic , Alan Schmitt
Interactive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_19⟩
Communication dans un congrès hal-01243017v1
Image document

Micro-Policies: Formally Verified, Tag-Based Security Monitors

 Arthur Azevedo de Amorim , Maxime Dénès , Nick Giannarakis , Cătălin Hriţcu , Benjamin C. Pierce , et al.
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, ⟨10.1109/SP.2015.55⟩
Communication dans un congrès hal-01265666v1
Image document

Proof reconstruction (preliminary version).

 Judicael Courant
[Research Report] LIP 1996-26, Laboratoire de l'informatique du parallélisme. 1996, 2+14p
Rapport hal-02101787v1
Image document

Verified programming and secure integration of operating system libraries in Coq

 Shenghao Yuan
Systems and Control [cs.SY]. Université de Rennes, 2023. English. ⟨NNT : 2023URENS060⟩
Thèse tel-04405955v1
Image document

Semantics of Probabilistic Programs using s-Finite Kernels in Coq

 Reynald Affeldt , Cyril Cohen , Ayumu Saito
CPP 2023 - Certified Programs and Proofs, Jan 2023, Boston, United States. ⟨10.1145/3573105.3575691⟩
Communication dans un congrès hal-03917948v1
Image document

A formal exploration of Nominal Kleene Algebra

 Paul Brunet , Damien Pous
MFCS, Aug 2016, Cracovie, Poland. ⟨10.4230/LIPIcs.MFCS.2016.22⟩
Communication dans un congrès hal-01307532v2
Image document

Automatic Transformation from Ecore Metamodels towards Gallina Inductive Types

 Jeremy Buisson , Seidali Rehab
MODELSWARD 2018, Jan 2018, Santa Cruz, Portugal. ⟨10.5220/0006608604880495⟩
Communication dans un congrès hal-01693939v1
Image document

A Formal Correctness Proof for an EDF Scheduler Implementation

 Florian Vanhems , Vlad Rusu , David Nowak , Gilles Grimaud
RTAS 2022: 28th IEEE Real-Time and Embedded Technology and Applications Symposium, May 2022, Milan, Italy. ⟨10.1109/RTAS54340.2022.00030⟩
Communication dans un congrès hal-03671598v2
Image document

Challenges in the collaborative development of a complex mathematical software and its ecosystem

 Théo Zimmermann
OpenSym 2018 - 14th International Symposium on Open Collaboration, Aug 2018, Paris, France. ⟨10.1145/3233391.3233966⟩
Communication dans un congrès hal-01951322v1
Image document

Certification of an Instruction Set Simulator

 Xiaomu Shi
Systèmes embarqués. Université de Grenoble, 2013. Français. ⟨NNT : ⟩
Thèse tel-00937524v1
Image document

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

 Frédéric Blanqui , Adam Koprowski
Mathematical Structures in Computer Science, 2011, 21 (4), pp.827-859. ⟨10.1017/S0960129511000120⟩
Article dans une revue inria-00543157v1
Image document

Prototype d'extension du système Coq

 Frédéric Blanqui
[Contrat] A04-R-505 || blanqui04e, 2004, 8 p
Rapport inria-00099932v1
Image document

A formal quantifier elimination for algebraically closed fields

 Cyril Cohen , Assia Mahboubi
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. pp.189-203, ⟨10.1007/978-3-642-14128-7_17⟩
Communication dans un congrès inria-00464237v3
Image document

CoLoR: a Coq library on rewriting and termination

 Frédéric Blanqui , Solange Coupet-Grimal , William Delobel , Sébastien Hinderer , Adam Koprowski
Eighth International Workshop on Termination - WST 2006, Aug 2006, Seattle, United States
Communication dans un congrès inria-00084835v2
Image document

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

 Cyril Cohen , Assia Mahboubi
Logical Methods in Computer Science, 2012, 8 (1:02), pp.1-40. ⟨10.2168/LMCS-8(1:02)2012⟩
Article dans une revue inria-00593738v4
Image document

Formalization and closedness of finite dimensional subspaces

 Florian Faissole
SYNASC 2017 - 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2017, Timișoara, Romania. pp.1-7
Communication dans un congrès hal-01630411v1
Image document

Towards an Independent Version of Tarski's System of Geometry

 Pierre Boutry , Stéphane Kastenbaum , Clément Saintier
14th International Conference on Automated Deduction in Geometry, Sep 2023, Belgrade, Serbia. pp.73-84, ⟨10.4204/EPTCS.398.11⟩
Communication dans un congrès hal-04324071v1
Image document

A Coq Formalization of the Bochner integral

 Sylvie Boldo , François Clément , Louise Leclerc
[Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022
Rapport hal-03516749v2
Image document

Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq

 Dominique Larchey-Wendling
6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), Jul 2021, Buenos Aires, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.18⟩
Communication dans un congrès hal-03280264v1
Image document

Proof Pearl: Faithful Computation and Extraction of µ-Recursive Algorithms in Coq

 Dominique Larchey-Wendling , Jean-François Monin
14th International Conference on Interactive Theorem Proving (ITP 2023), Adam Naumowicz; René Thiemann, Jul 2023, Białystok, Poland. pp.21:1--17, ⟨10.4230/LIPIcs.ITP.2023.21⟩
Communication dans un congrès hal-04200527v1
Page :