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

Filtrer vos résultats

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

Efficient Extensional Binary Tries

 Andrew W Appel , Xavier Leroy
Journal of Automated Reasoning, 2023, 67, pp.Article number 8. ⟨10.1007/s10817-022-09655-x⟩
Article dans une revue hal-03372247v4
Image document

Coqcots & Pycots: non-stopping components for safe dynamic reconfiguration

 Jérémy Buisson , Everton Calvacante , Fabien Dagnat , Elena Leroux , Sébastien Martinez
CBSE 2014 : proceedings of the 17th international ACM Sigsoft symposium on Component-based software engineering, Jun 2014, Lille, France. pp.1, ⟨10.1145/2602458.2602459⟩
Communication dans un congrès hal-00984365v1
Image document

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

 Sylvie Boldo , François Clément , Florian Faissole , Vincent Martin , Micaela Mayero
[Research Report] RR-9401, Inria, France. 2021, pp.38
Rapport hal-03194113v2
Image document

Hilbert's Tenth Problem in Coq (Extended Version)

 Dominique Larchey-Wendling , Yannick Forster
Logical Methods in Computer Science, 2022, 18 (1), ⟨10.46298/lmcs-18(1:35)2022⟩
Article dans une revue hal-03359505v2
Image document

A Formal Proof in Coq of a Control Function for the Inverted Pendulum

 Damien Rouhling
CPP 2018 - 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. pp.1-14, ⟨10.1145/3167101⟩
Communication dans un congrès hal-01639819v2
Image document

Définition de la classe de réécriture à intégrer

 Frédéric Blanqui
[Contrat] A04-R-487 || blanqui04c, 2004, 7 p
Rapport inria-00099930v1
Image document

A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq

 Pieter Collins , Milad Niqui , Nathalie Revol
NSV-3: Third International Workshop on Numerical Software Verification., Fainekos, Georgios and Goubault, Eric and Putot, Sylvie, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00473270v1
Image document

Formal Proofs of Rounding Error Bounds

 Pierre Roux
Journal of Automated Reasoning, 2015, pp.23. ⟨10.1007/s10817-015-9339-z⟩
Article dans une revue hal-01091189v2
Image document

System-level Non-interference for Constant-time Cryptography

 Gilles Barthe , Gustavo Betarte , Juan Diego Campo , Carlos Luna , David Pichardie
ACM SIGSAC Conference on Computer and Communications Security, CCS'14, Nov 2014, Scottsdale, United States. pp.1267 - 1279, ⟨10.1145/2660267.2660283⟩
Communication dans un congrès hal-01101950v1
Image document

Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi λProlog dialect)

 Enrico Tassi
The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles (CA), United States
Communication dans un congrès hal-01637063v1
Image document

Towards Verifying Declarative Netlog Protocols with Coq

 Yuxin Deng , Stéphane Grumbach , Jean-François Monin
[Intern report] 2010, pp.20
Rapport inria-00506093v1
Image document

Vérification formelle d'extractions de racines entières

 Yves Bertot
Revue 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
Image document

Short proof of Menger's Theorem in Coq (Proof Pearl)

 Christian Doczkal
2019
Pré-publication, Document de travail hal-02086931v1
Image document

On the Use of Formal Methods to Model and Verify Neuronal Archetypes

 Elisabetta de Maria , Abdorrahim Bahrami , Thibaud L'Yvonnet , Amy Felty , Daniel Gaffé , et al.
Frontiers of Computer Science, 2021, 16, pp.28
Article dans une revue hal-03053930v1
Image document

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography

 Philipp G Haselwarter , Benjamin Salling Hvass , Lasse Letager Hansen , Théo Winterhalter , Cătălin Hriţcu , et al.
CPP 2024 - 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2024, London, United Kingdom. pp.30-44, ⟨10.1145/3636501.3636961⟩
Communication dans un congrès hal-04484598v1
Image document

Managing Logical and Computational Complexity using Program Transformations

 Nicolas Tabareau
Category Theory [math.CT]. université de nantes, 2016
HDR tel-01406351v1
Image document

A new Type-Class solver for Coq in Elpi

 Davide Fissore , Enrico Tassi
The Coq Workshop 2023, Jul 2023, Białystok, Poland
Communication dans un congrès hal-04467855v1
Image document

Accurate calculation of Euclidean Norms using Double-word arithmetic

 Vincent Lefèvre , Nicolas Louvet , Jean-Michel Muller , Joris Picot , Laurence Rideau
ACM Transactions on Mathematical Software, 2023, 49 (1), pp.1-34. ⟨10.1145/3568672⟩
Article dans une revue hal-03482567v2
Image document

Unsolvability of the Quintic Formalized in Dependent Type Theory

 Sophie Bernard , Cyril Cohen , Assia Mahboubi , Pierre-Yves Strub
ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France
Communication dans un congrès hal-03136002v4
Image document

Lawvere-Tierney sheafification in Homotopy Type Theory

 Kevin Quirin
Logic in Computer Science [cs.LO]. Ecole des Mines de Nantes, 2016. English. ⟨NNT : 2016EMNA0298⟩
Thèse tel-01486550v1
Image document

Compilation of Linearizable Data Structures

 Yannick Zakowski , David Cachera , Delphine Demange , David Pichardie
[Research Report] ENS Rennes; IRISA, Inria Rennes; Université Rennes 1. 2017
Rapport hal-01538128v1
Image document

Reliably Reproducing Machine-Checked Proofs with the Coq Platform

 Karl Palmskog , Enrico Tassi , Théo Zimmermann
RRRR 2022 - Workshop on Reproducibility and Replication of Research Results, Apr 2022, Munich, Germany
Communication dans un congrès hal-03592675v2
Image document

Verification of a Concurrent Garbage Collector

 Yannick Zakowski
Data Structures and Algorithms [cs.DS]. École normale supérieure de Rennes, 2017. English. ⟨NNT : 2017ENSR0010⟩
Thèse tel-01680213v2
Image document

CoqTL: an Internal DSL for Model Transformation in Coq

 Massimo Tisi , Zheng Cheng
ICMT 2018 - 11th International Conference on Theory and Practice of Model Transformations, Jun 2018, Toulouse, France. pp.142-156, ⟨10.1007/978-3-319-93317-7_7⟩
Communication dans un congrès hal-01828344v1
Image document

Construction of real algebraic numbers in Coq

 Cyril Cohen
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States
Communication dans un congrès hal-00671809v2
Image document

Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq.

 Elie Soubiran
Langage de programmation [cs.PL]. Ecole Polytechnique X, 2010. Français. ⟨NNT : ⟩
Thèse tel-00679201v1
Image document

Generation of Inductive Types from Ecore Metamodels

 Jérémy Buisson , Seidali Rehab
Model-Driven Engineering and Software Development. MODELSWARD 2018., pp.308-334, 2019
Chapitre d'ouvrage hal-02021361v1
Image document

Formal Proof of Soundness for an RL Prover

 Andrei Arusoaie , David Nowak , Vlad Rusu , Dorel Lucanu
[Technical Report] RR-0471, INRIA Lille - Nord Europe; Alexandru Ioan Cuza, University of Iasi. 2015, pp.27
Rapport hal-01244578v1
Image document

Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)

 Amin Timany , Matthieu Sozeau
[Research Report] RR-9105, KU Leuven, Belgium; Inria Paris. 2017, pp.32
Rapport hal-01615123v3
Image document

Deciding Kleene Algebras in Coq

 Thomas Braibant , Damien Pous
ITP, Aug 2010, Edinburgh, United Kingdom. pp.163-178, ⟨10.1007/978-3-642-14052-5_13⟩
Communication dans un congrès hal-00383070v5
Page :