Academic literature on the topic 'Coq (assistant de preuve)'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Coq (assistant de preuve).'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Journal articles on the topic "Coq (assistant de preuve)"
1
Gäher, Lennard, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer. "RefinedRust: A Type System for High-Assurance Verification of Rust Programs." Proceedings of the ACM on Programming Languages 8, PLDI (June 20, 2024): 1115–39. http://dx.doi.org/10.1145/3656422.
Full textAbstract:
Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a general-purpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code.
2
Zhou, Litao, Jianxing Qin, Qinshi Wang, Andrew W. Appel, and Qinxiang Cao. "VST-A: A Foundationally Sound Annotation Verifier." Proceedings of the ACM on Programming Languages 8, POPL (January 5, 2024): 2069–98. http://dx.doi.org/10.1145/3632911.
Full textAbstract:
Program verifiers for imperative languages such as C may be annotation-based, in which assertions and invariants are put into source files and then checked, or tactic-based, where proof scripts separate from programs are interactively developed in a proof assistant such as Coq. Annotation verifiers have been more automated and convenient, but some interactive verifiers have richer assertion languages and formal proofs of soundness. We present VST-A, an annotation verifier that uses the rich assertion language of VST, leverages the formal soundness proof of VST, but allows users to describe functional correctness proofs intuitively by inserting assertions. VST-A analyzes control flow graphs, decomposes every C function into control flow paths between assertions, and reduces program verification problems into corresponding straightline Hoare triples. Compared to existing foundational program verification tools like VST and Iris, in VST-A such decompositions and reductions can nonstructural, which makes VST-A more flexible to use. VST-A's decomposition and reduction is defined in Coq, proved sound in Coq, and computed call-by-value in Coq. The soundness proof for reduction is totally logical, independent of the complicated semantic model (and soundness proof) of VST's Hoare triple. Because of the rich assertion language, not all reduced proof goals can be automatically checked, but the system allows users to prove residual proof goals using the full power of the Coq proof assistant.
3
VOEVODSKY, VLADIMIR. "An experimental library of formalized Mathematics based on the univalent foundations." Mathematical Structures in Computer Science 25, no. 5 (January 20, 2015): 1278–94. http://dx.doi.org/10.1017/s0960129514000577.
Full textAbstract:
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
4
MAHBOUBI, ASSIA. "Implementing the cylindrical algebraic decomposition within the Coq system." Mathematical Structures in Computer Science 17, no. 1 (February 2007): 99–127. http://dx.doi.org/10.1017/s096012950600586x.
Full textAbstract:
The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.
5
Zúñiga, Angel, and Gemma Bel-Enguix. "Coinductive Natural Semantics for Compiler Verification in Coq." Mathematics 8, no. 9 (September 12, 2020): 1573. http://dx.doi.org/10.3390/math8091573.
Full textAbstract:
(Coinductive) natural semantics is presented as a unifying framework for the verification of total correctness of compilers in Coq (with the feature that a verified compiler can be obtained). In this way, we have a simple, easy, and intuitive framework; to carry out the verification of a compiler, using a proof assistant in which both cases are considered: terminating and non-terminating computations (total correctness).
6
Wang, Qian, Xiaoyu Song, Ming Gu, and Jiaguang Sun. "Functional Verification of High Performance Adders in COQ." Journal of Applied Mathematics 2014 (2014): 1–9. http://dx.doi.org/10.1155/2014/197252.
Full textAbstract:
Addition arithmetic design plays a crucial role in high performance digital systems. The paper proposes a systematic method to formalize and verify adders in a formal proof assistant COQ. The proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry, in a faithful, scalable, and modularized way. The methodology can be extended to other adder architectures as well.
7
Forster, Yannick, Dominik Kirst, and Dominik Wehr. "Completeness theorems for first-order logic analysed in constructive type theory." Journal of Logic and Computation 31, no. 1 (January 2021): 112–51. http://dx.doi.org/10.1093/logcom/exaa073.
Full textAbstract:
Abstract We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak Kőnig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.
8
PELAYO, ÁLVARO, VLADIMIR VOEVODSKY, and MICHAEL A. WARREN. "A univalent formalization of the p-adic numbers." Mathematical Structures in Computer Science 25, no. 5 (February 13, 2015): 1147–71. http://dx.doi.org/10.1017/s0960129514000541.
Full textAbstract:
The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.
9
Sacchini, Jorge Luis. "Towards a New Termination Checker for the Coq Proof Assistant." Qatar Foundation Annual Research Forum Proceedings, no. 2011 (November 2011): CSP23. http://dx.doi.org/10.5339/qfarf.2011.csp23.
Full text
10
Huet, Gérard. "Residual theory in λ-calculus: a formal development." Journal of Functional Programming 4, no. 3 (July 1994): 371–94. http://dx.doi.org/10.1017/s0956796800001106.
Full textAbstract:
AbstractWe present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.
Dissertations / Theses on the topic "Coq (assistant de preuve)"
1
Lelay, Catherine. "Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée." Thesis, Paris 11, 2015. http://www.theses.fr/2015PA112096/document.
Full textAbstract:
L'analyse réelle a de nombreuses applications car c'est un outil approprié pour modéliser de nombreux phénomènes physiques et socio-économiques. En tant que tel, sa formalisation dans des systèmes de preuve formelle est justifié pour permettre aux utilisateurs de vérifier formellement des théorèmes mathématiques et l'exactitude de systèmes critiques. La bibliothèque standard de Coq dispose d'une axiomatisation des nombres réels et d'une bibliothèque de théorèmes d'analyse réelle. Malheureusement, cette bibliothèque souffre de nombreuses lacunes. Par exemple, les définitions des intégrales et des dérivées sont basées sur les types dépendants, ce qui les rend difficiles à utiliser dans la pratique. Cette thèse décrit d'abord l'état de l'art des différentes bibliothèques d'analyse réelle disponibles dans les assistants de preuve. Pour pallier les insuffisances de la bibliothèque standard de Coq, nous avons conçu une bibliothèque facile à utiliser : Coquelicot. Une façon plus facile d'écrire les formules et les théorèmes a été mise en place en utilisant des fonctions totales à la place des types dépendants pour écrire les limites, dérivées, intégrales et séries entières. Pour faciliter l'utilisation, la bibliothèque dispose d'un ensemble complet de théorèmes couvrant ces notions, mais aussi quelques extensions comme les intégrales à paramètres et les comportements asymptotiques. En plus, une hiérarchie algébrique permet d'appliquer certains théorèmes dans un cadre plus générique comme les nombres complexes pour les matrices. Coquelicot est une extension conservative de l'analyse classique de la bibliothèque standard de Coq et nous avons démontré les théorèmes de correspondance entre les deux formalisations. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur une épreuve du Baccalauréat, pour les définitions et les propriétés des fonctions de Bessel ainsi que pour la solution de l'équation des ondes en dimension 1Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals and asymptotic behaviors. Moreover, an algebraic hierarchy makes it possible to apply some of the theorems in a more generic setting, such as complex numbers or matrices. Coquelicot is a conservative extension of the classical analysis of Coq's standard library and we provide correspondence theorems between the two formalizations. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation
2
Sall, Boubacar Demba. "Programmation impérative par raffinements avec l'assistant de preuve Coq." Electronic Thesis or Diss., Sorbonne université, 2020. http://www.theses.fr/2020SORUS181.
Full textAbstract:
Cette thèse s’intéresse à la programmation certifiée correcte dans le cadre formel fourni par l’assistant de preuve Coq, et conduite par étapes de raffinements, avec l'objectif d’aboutir à un résultat correct par construction. Le langage de programmation considéré est un langage impératif simple, avec affectations, alternatives, séquences, et boucles. La sémantique associée à ce langage est une sémantique relationnelle exprimée dans un cadre prédicatif plus adapté à un plongement dans la théorie des types, plutôt que dans le calcul des relations. Nous étudions la relation entre d’une part la sémantique prédicative et relationnelle que nous avons choisie, et d’autre part une approche plus classique dans le style de la logique de Hoare. En particulier, nous montrons que les deux approches ont en théorie la même puissance. La démarche que nous étudions consiste à certifier, avec l’aide d’un assistant de preuve, les raffinements successifs permettant de passer de la spécification au programme. Nous nous intéressons donc aussi aux techniques de preuve permettant en pratique d’établir la validité des raffinements. Plus précisément, nous utilisons un calcul de la plus faible pré-spécification jouant ici le rôle du calcul de la plus faible pré-condition dans les approches classiques. Afin que l’articulation des étapes de raffinement reste aussi proche que possible de l’activité de programmation, nous formalisons un langage de développement qui permet de décrire l’arborescence des étapes de raffinement, ainsi qu’une logique permettant de raisonner sur ces développements, et de garantir leur correctionThis thesis investigates certified programming by stepwise refinement in the framework of the Coq proof assistant. This allows the construction of programs that are correct by construction. The programming language that is considered is a simple imperative language with assignment, selection, sequence, and iteration. The semantics of this language is formalized in a relational and predicative setting, and is shown to be equivalent to an axiomatic semantics in the style of a Hoare logic. The stepwise refinement approach to programming requires that refinement steps from the specification to the program be proved correct. For so doing, we use a calculus of weakest pre-specifications which is a generalisation of the calculus of weakest pre-conditions. Finally, to capture the whole refinement history of a program development, we formalize a design language and a logic for reasoning about program designs in order to establish that all refinement steps are indeed correct. The approach developed during this thesis is entirely mecanised using the Coq proof assistant
3
Filou, Vincent. "Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq." Thesis, Bordeaux 1, 2012. http://www.theses.fr/2012BOR14708/document.
Full textAbstract:
L'objectif de cette thèse est de produire un environnement permettant de raisonner formellement sur la correction de systèmes de calculs locaux, ainsi que sur l'expressivité de ce modèle de calcul. Pour ce faire, nous utilisons l'assistant de preuve Coq. Notre première contribution est la formalisation en Coq de la sémantique des systèmes de réétiquetage localement engendrés, ou calculs locaux. Un système de calculs locaux est un système de réétiquetage de graphe dont la portée est limitée. Nous proposons donc tout d'abord une implantation succincte de la théorie des graphes en Coq, et utilisons cette dernière pour définir les systèmes de réétiquetage de graphes localement engendrés. Nous avons relevé, dans la définition usuelle des calculs locaux, certaines ambiguïtés. Nous proposons donc une nouvelle définition, et montrons formellement que celle-ci capture toutes les sous-classes d'algorithmes étudiées. Nous esquissons enfin une méthodologie de preuve des systèmes de calculs locaux en Coq.Notre seconde contribution consiste en l'étude formelle de l'expressivité des systèmes de calculs locaux. Nous formalisons un résultat de D. Angluin (repris par la suite par Y. Métivier et J. Chalopin): l'inexistence d'un algorithme d'élection universelle. Nous proposons ensuite deux lemmes originaux concernant les calculs locaux sur les arêtes (ou systèmes LC0), et utilisons ceux-ci pour produire des preuves formelles d'impossibilité pour plusieurs problèmes: calcul du degré de chaque sommet, calcul d'arbre recouvrant, etélection. Nous proposons informellement une nouvelles classes de graphe pour laquelle l'élection est irréalisable par des calculs locaux sur les arêtes.Nous étudions ensuite les transformations de systèmes de calculs locaux et de leur preuves. Nous adaptons le concept de Forward Simulation de N. Lynch aux systèmes de calculs locaux et utilisons ce dernier pour démontrer formellement l'inclusion de deux modes de détection de terminaison dans le cas des systèmes LC0. La preuve de cette inclusion estsimplifiée par l'utilisation de transformations "standards" de systèmes, pour lesquels des résultats génériques ont été démontrés. Finalement, nous réutilisons ces transformations standards pour étudier, en collaboration avec M. Tounsi, deux techniques de composition des systèmes de réétiquetage LC0. Une bibliothèque Coq d'environ 50000 lignes, contenant les preuves formelles des théorèmes présentés dans le mémoire de thèse à été produite en collaboration avec Pierre Castéran (dont environ 40%produit en propre par V. Filou) au cours de cette thèseThe goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran
4
Zucchini, Rébecca. "Bibliothèque certifiée en Coq pour la provenance des données." Electronic Thesis or Diss., université Paris-Saclay, 2023. http://www.theses.fr/2023UPASG040.
Full textAbstract:
La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. La thèse propose ainsi la formalisation de deux types de provenance des données couramment utilisés, la How-provenance et la Where-provenance. Cette formalisation a permis de comparer leur sémantique, mettant en évidence leurs différences et leurs complémentarités. En outre, elle a conduit à la proposition d'une structure algébrique et d'une sémantique unificatrice pour ces deux types de provenanceThis thesis is about the formalization of data provenance using the Coq proof assistant, at the intersection of formal methods and database communities. It explores the importance of data provenance, which tracks the origin and history of data, in addressing issues such as poor data quality, incorrect interpretations, and lack of transparency in data processing. The thesis proposes formalizations of two commonly used types of data provenance, How-provenance and Where-provenance. Formalizing both types of provenance allowed us to compare their semantics, highlighting their differences and complementarities. Additionally, the formalization of these two types of provenance led to the proposal of an algebraic structure that provides a unifying semantics
5
Braun, David. "Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective." Thesis, Strasbourg, 2019. http://www.theses.fr/2019STRAD020.
Full textAbstract:
Ce travail de thèse s’inscrit dans le domaine de la preuve assistée par ordinateur et se place d'un point de vue méthodologique. L’objectif premier des assistants de preuves est de vérifier qu’une preuve écrite à la main est correcte; la question ici est de savoir comment à l’intérieur d’un tel système, il est possible d'aider un utilisateur à fabriquer une preuve formelle du résultat auquel il s'intéresse. Ces questions autour de la vérification de preuves, en particulier en certification du logiciel, et au delà de leur traçabilité et de leur lisibilité sont en effet devenues prégnantes avec l’importance qu’ont prise les algorithmes dans notre société. Bien évidemment, répondre à la question de l’aide à la preuve dans toute sa généralité dépasse largement le cadre de cette thèse. C’est pourquoi nous focalisons nos travaux sur la preuve en mathématiques dans un cadre particulier qui est bien connu dans notre équipe : la géométrie et sa formalisation dans le système Coq. Dans ce domaine, nous mettons premièrement en évidence les niveaux auxquels on peut oeuvrer à savoir le contexte scientifique à travers les méthodes de formalisation mais aussi le contexte méthodologique et technique au sein de l'assistant de preuve Coq. Dans un second temps, nous essayons de montrer comment nos méthodes et nos idées sont généralisables à d'autres disciplines. Nous mettons ainsi en place dans nos travaux les premiers jalons pour une aide à la preuve efficace dans un contexte géométrique simple mais omniprésent. À travers une approche classique fondée sur la géométrie synthétique et une approche combinatoire complémentaire utilisant le concept de rang issu de la théorie des matroïdes, nous fournissons à l'utilisateur des principes généraux et des outils facilitant l'élaboration de preuves formelles. Dans ce sens, nous comparons les capacités d'automatisation de ces deux approches dans le contexte précis des géométries finies avant de finalement construire un prouveur automatique de configuration géométrique d'incidenceThis thesis work is part of the general field of computer-assisted proof and is methodologically based. The primary objective of proof assistants is to verify that handwritten demonstration is correct; the question here is how within such a system, it is possible to help a user to make a formal proof of the result in which he is interested. These questions around the verification of proofs, in particular in software certification, and beyond their traceability and readability have indeed become significant with the importance that algorithms have taken on in our society. Obviously, answering the question of proof assistance in all its generality goes far beyond the scope of this thesis. This is why we focus our work on proof in mathematics in a particular framework that is well known in our team: geometry and its formalization in the Coq system. In this field, we first highlight the levels at which we can work, namely the scientific context through the formalization methods but also the methodological and technical context within the Coq proof assistant. In a second step, we try to show how our methods and ideas can be generalized to other disciplines. In this way, we are putting in place the first steps towards effective proof assistance in a simple but omnipresent geometric context. Through a classical approach based on synthetic geometry and a complementary combinatorial approach using the concept of rank from matroid theory, we provide the user with general principles and tools to facilitate the development of formal proof. In this sense, we compare the automation capabilities of these two approaches in the specific context of finite geometries before finally constructing an automatic prover of geometric configurations of incidence
6
Mouhcine, Houda. "Formal Proofs in Applied Mathematics : A Coq Formalization of Simplicial Lagrange Finite Elements." Electronic Thesis or Diss., université Paris-Saclay, 2024. https://theses.hal.science/tel-04884651.
Full textAbstract:
Cette thèse est dédiée au développement de preuves formelles de théorèmes et propositions mathématiques dans le domaine de l'analyse réelle, en utilisant l'assistant de preuve Coq pour garantir leur exactitude. Le cœur de ce travail est divisé en deux parties principales.La première partie se concentre sur l'utilisation de Coq pour formaliser des principes mathématiques clés tels que le principe d'induction de Lebesgue et le théorème de Tonelli, permettant le calcul d'intégrales doubles sur des espaces produits en intégrant de manière itérative par rapport à chaque variable. Ce travail s'appuie sur des recherches antérieures en théorie de la mesure et sur l'intégrale de Lebesgue.La deuxième partie de cette thèse fonctionne dans le cadre de la méthode des éléments finis (MEF), une technique numérique largement utilisée pour résoudre des équations aux dérivées partielles (EDP). La MEF joue un rôle important dans de nombreux programmes de simulation industrielle, notamment dans l'approximation des solutions à des problèmes complexes tels que le transfert de chaleur, la dynamique des fluides et les simulations de champs électromagnétiques. Plus spécifiquement, nous visons à construire des éléments finis, en nous concentrant sur les éléments finis de Lagrange simpliciaux avec des degrés de liberté répartis uniformément. Ce travail mobilise un large éventail de concepts algébriques, y compris les familles finies, les monoïdes, les espaces vectoriels, les espaces affines, les sous-structures et les espaces de dimensions finies.Pour mener à bien cette étude, nous formalisons dans Coq en logique classique plusieurs composants fondamentaux. Nous commençons par construire un élément fini général, puis nous procédons à la définition de plusieurs composants fondamentaux, y compris la construction de l'espace d'approximation de Lagrange, l'expression de sa base de polynômes de Lagrange et la formalisation des transformations géométriques affines et de la propriété d'unisolvance des éléments finis de LagrangeThis thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts.The first part focuses on using Coq to formalize key mathematical principles such as the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral.The second part of this thesis operates within the framework of the Finite Element Method (FEM), a widely used numerical technique for solving partial differential equations (PDEs). FEM plays an important role in numerous industrial simulation programs, particularly in approximating solutions to complex problems such as heat transfer, fluid dynamics, and electromagnetic field simulations. Specifically, we aim to construct finite elements, focusing on simplicial Lagrange finite elements with evenly distributed degrees of freedom. This work engages a broad range of algebraic concepts, including finite families, monoids, vector spaces, affine spaces, substructures, and finite-dimensional spaces.To conduct this study, we formalize in Coq in classical logic several foundational components. We begin by constructing a general finite element, then proceed to define several foundational components, including the construction of the Lagrange approximation space, expressing its Lagrange polynomial basis, and formalizing affine geometric transformations and the unisolvence property of Lagrange finite elements
7
Dubois, De Prisque Louise. "Prétraitement compositionnel en Coq." Electronic Thesis or Diss., université Paris-Saclay, 2024. http://www.theses.fr/2024UPASG040.
Full textAbstract:
Cette thèse présente une méthodologie de prétraitement visant à transformer certains énoncés de la logique de l'assistant de preuve Coq en énoncés de logique du premier ordre, de façon à les envoyer à des prouveurs automatiques, et en particulier des prouveurs SMT. Cette méthodologie consiste à composer de petites transformations indépendantes et certifiantes, prenant la forme de tactiques Coq. Une implémentation de cette méthodologie est proposée dans un plugin appelé Sniper, qui offre une tactique "pousse-bouton" d'automatisation. Par ailleurs, un ordonnanceur de transformations logiques permet d'ajouter ses propres transformations logiques à l'ensemble et de déterminer quelles transformations s'appliquent en fonction de la preuve à effectuerThis thesis presents a preprocessing methodology aimed at transforming certain statements from the Coq proof assistant's logic into first-order logic statements, in order to send them to automatic provers, in particular SMT solvers. This methodology involves composing small, independent, and certifying transformations, taking the form of Coq tactics. An implementation of this methodology is provided in a plugin called Sniper, which offers a "push-button" automation tactic. Furthermore, a logical transformation scheduler (called Orchestrator) allows adding one's own logical transformations and determines which transformations apply depending on the proof to be carried out
8
Keller, Chantal. "A Matter of Trust : Skeptical Communication between Coq and External Provers." Palaiseau, Ecole polytechnique, 2013. http://pastel.archives-ouvertes.fr/docs/00/83/83/22/PDF/thesis-keller.pdf.
Full textAbstract:
Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificatsThis thesis studies the cooperation between the Coq proof assistant and external provers through proof witnesses. We concentrate on two different kinds of provers that can return certicates: first, answers coming from SAT and SMT solvers can be checked in Coq to increase both the confidence in these solvers and Coq's automation; second, theorems established in interactive provers based on Higher-Order Logic can be exported to Coq and checked again, in order to offer the possibility to produce formal developments which mix these two dierent logical paradigms. It ended up in two software: SMTCoq, a bi-directional cooperation between Coq and SAT/SMT solvers, and HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq. For both tools, we took great care to define a modular and efficient architecture, based on three clearly separated ingredients: an embedding of the formalism of the external tool inside Coq which is carefully translated into Coq terms, a certified checker to establish the proofs using the certicates, and an Ocaml preprocessor to transform proof witnesses coming from different provers into a generic certificate. This division allows that a change in the format of proof witnesses only affects the preprocessor, but no proved Coq code. Another fundamental component for efficiency and modularity is computational reflection, which exploits the computational power of Coq to establish generic and small proofs based on the certicates
9
Paulin-Mohring, Christine. "Définitions Inductives en Théorie des Types." Habilitation à diriger des recherches, Université Claude Bernard - Lyon I, 1996. http://tel.archives-ouvertes.fr/tel-00431817.
Full textAbstract:
Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il présente, étudie et justifie les choix faits dans le système Coq.
10
Herms, Paolo. "Certification of a Tool Chain for Deductive Program Verification." Phd thesis, Université Paris Sud - Paris XI, 2013. http://tel.archives-ouvertes.fr/tel-00789543.
Full textAbstract:
This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements, the specification. This is especiallyimportant for critical computer programs, such as control systems forair planes, trains and power plants. Here a malfunctioning occurringduring operation would have catastrophic consequences. Software requirements can concern safety or functioning. Safetyrequirements, such as not accessing memory locations outside validbounds, are often implicit, in the sense that any implementation isexpected to be safe. On the other hand, functional requirementsspecify what the program is supposed to do. The specification of aprogram is often expressed informally by describing in English or someother natural language the mission of a part of the program code.Usually program verification is then done by manual code review,simulation and extensive testing. But this does not guarantee that allpossible execution cases are captured. Deductive program proving is a complete way to ensure soundness of theprogram. Here a program along with its specificationis a mathematical object and its desired properties are logicaltheorems to be formally proved. This way, if the underlying logicsystem is consistent, we can be absolutely sure that the provenproperty holds for the program in any case.Generation of verification conditions is a technique helpingthe programmer to prove the properties he wants about his programs.Here a VCG tool analyses a program and its formal specification andproduces a mathematical formula, whose validity implies the soundnessof the program with respect to its specification. This is particularlyinteresting when the generated formulas can be proved automatically byexternal SMT solvers.This approach is based on works of Hoare and Dijkstra and iswell-understood and shown correct in theory. Deductive verificationtools have nowadays reached a maturity allowing them to be used inindustrial context where a very high level of assurance isrequired. But implementations of this approach must deal with allkinds of language features and can therefore become quite complex andcontain errors -- in the worst case stating that a program correcteven if it is not. This raises the question of the level ofconfidence granted to these tools themselves. The aim of this thesis is to address this question. We develop, inthe Coq system, a certified verification-condition generator (VCG) forACSL-annotated C programs.Our first contribution is the formalisation of an executableVCG for the Whycert intermediate language,an imperative language with loops, exceptions and recursive functionsand its soundness proof with respect to the blocking big-step operational semantics of the language.A second contribution is the formalisation of the ACSL logicallanguage and the semantics of ACSL annotations of Compcert's Clight.From the compilation of ACSL annotated Clight programs to Whycertprograms and its semantics preservation proof combined with a Whycertaxiomatisation of the Compcert memory model results our maincontribution: an integrated certified tool chainfor verification of C~programs on top of Compcert. By combining oursoundness result with the soundness of the Compcert compiler we obtaina Coq theorem relating the validity of the generated proof obligationswith the safety of the compiled assembly code.
Books on the topic "Coq (assistant de preuve)"
1
Chlipala, Adam. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
Find full text
2
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2022.
Find full text
3
Chlipala, Adam. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
Find full text
4
Chlipala, Adam. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press, 2013.
Find full text
5
Chlipala, Adam. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
Find full textBook chapters on the topic "Coq (assistant de preuve)"
1
Ekici, Burak, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, and Clark Barrett. "Formal Verification of Bit-Vector Invertibility Conditions in Coq." In Frontiers of Combining Systems, 41–59. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-43369-6_3.
Full textAbstract:
AbstractWe prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. Previous work proved many of these in a completely automatic fashion for arbitrary bit-width; however, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over larger bit-widths. In this paper we describe the process of proving a representative subset of these invertibility conditions in Coq. In particular, we describe the library for bit-vectors in Coq, our extensions to it, and proofs of the invertibility conditions.
2
Benzmüller, Christoph, and Bruno Woltzenlogel Paleo. "Interacting with Modal Logics in the Coq Proof Assistant." In Lecture Notes in Computer Science, 398–411. Cham: Springer International Publishing, 2015. http://dx.doi.org/10.1007/978-3-319-20297-6_25.
Full text
3
Bosser, Anne-Gwenn, Pierre Courtieu, Julien Forest, and Marc Cavazza. "Structural Analysis of Narratives with the Coq Proof Assistant." In Interactive Theorem Proving, 55–70. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011. http://dx.doi.org/10.1007/978-3-642-22863-6_7.
Full text
4
Castro, David, Francisco Ferreira, and Nobuko Yoshida. "EMTST: Engineering the Meta-theory of Session Types." In Tools and Algorithms for the Construction and Analysis of Systems, 278–85. Cham: Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-45237-7_17.
Full textAbstract:
Abstract Session types provide a principled programming discipline for structured interactions. They represent a wide spectrum of type-systems for concurrency. Their type safety is thus extremely important. EMTST is a tool to aid in representing and validating theorems about session types in the Coq proof assistant. On paper, these proofs are often tricky, and error prone. In proof assistants, they are typically long and difficult to prove. In this work, we propose a library that helps validate the theory of session types calculi in proof assistants. As a case study, we study two of the most used binary session types systems: we show the impossibility of representing the first system in $$\alpha $$-equivalent representations, and we prove type preservation for the revisited system. We develop our tool in the Coq proof assistant, using locally nameless for binders and small scale reflection to simplify the handling of linear typing environments.
5
Paulin-Mohring, Christine. "Introduction to the Coq Proof-Assistant for Practical Software Verification." In Lecture Notes in Computer Science, 45–95. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-35746-6_3.
Full text
6
Oury, Nicolas. "Observational Equivalence and Program Extraction in the Coq Proof Assistant." In Lecture Notes in Computer Science, 271–85. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003. http://dx.doi.org/10.1007/3-540-44904-3_19.
Full text
7
Bartzia, Evmorfia-Iro, and Pierre-Yves Strub. "A Formal Library for Elliptic Curves in the Coq Proof Assistant." In Interactive Theorem Proving, 77–92. Cham: Springer International Publishing, 2014. http://dx.doi.org/10.1007/978-3-319-08970-6_6.
Full text
8
Reynolds, Conor. "Formalizing the Institution for Event-B in the Coq Proof Assistant." In Rigorous State-Based Methods, 162–66. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-77543-8_17.
Full textAbstract:
AbstractWe formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution "Image missing" for Event-B, and its relationship with the institution "Image missing" for first-order predicate logic. We prove the satisfaction condition for "Image missing" and encode the institution comorphism "Image missing" embedding "Image missing" in "Image missing" .
9
Alves, Thayonara, Leopoldo Teixeira, Vander Alves, and Thiago Castro. "Porting the Software Product Line Refinement Theory to the Coq Proof Assistant." In Lecture Notes in Computer Science, 192–209. Cham: Springer International Publishing, 2020. http://dx.doi.org/10.1007/978-3-030-63882-5_12.
Full text
10
Albert, Elvira, Samir Genaim, Daniel Kirchner, and Enrique Martin-Martin. "Formally Verified EVM Block-Optimizations." In Computer Aided Verification, 176–89. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-37709-9_9.
Full textAbstract:
AbstractThe efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on (Ethereum Virtual Machine) block-optimizations, which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two blocks under comparison.Artifact:https://doi.org/10.5281/zenodo.7863483
Conference papers on the topic "Coq (assistant de preuve)"
1
Berramla, Karima, El Abbassia Deba, and Mohammed Senouci. "Formal validation of model transformation with Coq proof assistant." In 2015 First International Conference on New Technologies of Information and Communication (NTIC). IEEE, 2015. http://dx.doi.org/10.1109/ntic.2015.7368755.
Full text
2
Chernenko, Ivan, Igor Anureev, and Natalia Garanina. "Proving Reflex Program Verification Conditions in Coq Proof Assistant." In 2021 IEEE 22nd International Conference of Young Professionals in Electron Devices and Materials (EDM). IEEE, 2021. http://dx.doi.org/10.1109/edm52169.2021.9507628.
Full text
3
Lei, Siran, Mengqi Cheng, and Jianguo jiang. "Tactics for Proving Separation Logic Assertion in Coq Proof Assistant." In ICVISP 2019: 3rd International Conference on Vision, Image and Signal Processing. New York, NY, USA: ACM, 2019. http://dx.doi.org/10.1145/3387168.3387257.
Full text
4
Mackay, Julian, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas Cameron. "Encoding Featherweight Java with assignment and immutability using the Coq proof assistant." In the 14th Workshop. New York, New York, USA: ACM Press, 2012. http://dx.doi.org/10.1145/2318202.2318206.
Full text
5
Leme, Renato R., Giorgio Venturi, and Bruno Lopes. "Coq Formalization of a Tableau for the Classical-Intuitionistic Propositional Fragment of Ecumenical Logic." In Workshop Brasileiro de Lógica. Sociedade Brasileira de Computação, 2022. http://dx.doi.org/10.5753/wbl.2022.223071.
Full text
6
Silva, Guilherme G. F. da, Edward Hermann Haeusler, and Cláudia Nalon. "Description of Command and Control Networks in Coq." In Workshop-Escola de Informática Teórica. Sociedade Brasileira de Computação, 2021. http://dx.doi.org/10.5753/weit.2021.18923.
Full textAbstract:
A command and control (C2) system can be defined as a group of individuals organised hierarchically in which higher-ranking individuals can issuedirections to their subordinates with a certain goal in mind. We present a model for representation of command and control networks in the Coq proof assistant based on a tree data structure. Our model utilises Coq’s implementation of data structures and includes examples of how to define functions and properties that may be relevant in a C2 system, as well as examples of some of the tests we have performed to verify the correctness and usability of our model. The examples given here are simple, but constitute basic blocks that can later be used in more realistic formalisations.
7
Guo, Dakai, Qiming Wang, Jianghao Liu, and Wensheng Yu. "Formalizing the Term Substitution Theorem in First-Order Logic within the Coq Proof Assistant." In 2023 China Automation Congress (CAC). IEEE, 2023. http://dx.doi.org/10.1109/cac59555.2023.10450918.
Full text
8
Freitas, Francisco Aislan da Silva, Bruno Da Silva Queiroz, Cassandra Ribeiro Joye, and Paulo Henrique Mendes Maia. "ASSIS: Assistente Inteligente como Serviço para Plataformas de Ensino a Distância." In Simpósio Brasileiro de Informática na Educação. Sociedade Brasileira de Computação, 2020. http://dx.doi.org/10.5753/cbie.sbie.2020.1423.
Full textAbstract:
A evasão escolar ocorre em diversas modalidades de ensino, ocasionando perdas à todos envolvidos no processo educacional. Mapear, minerar e tratar o comportamento dos estudantes a partir de indicadores é possível com técnicas de Inteligência Artificial integradas numa solução como o ASSIS ,um Assistente Inteligente como serviço para plataformas de ensino a distância. Este artigo apresenta como foi desenvolvida, aplicada e validada uma estrutura para prever situações de potencial de evasão escolar usando como metodologia técnicas de aprendizagem de máquina com características comportamentais dos estudantes nas plataformas EaD. O melhor modelo de IA foi o Support Vector Machine, para o qual os parâmetros Accuracy, F Score, Recall e Precision obtiveram os resultados 95,84%, 95,79%, 94,74% e 96,88%, respectivamente.