Bibliographies thématiques / Coq formalization

Sommaire

Articles de revues
Thèses
Livres
Chapitres de livres
Actes de conférences

Littérature scientifique sur le sujet « Coq formalization »

Auteur : Grafiati

Publié le 2 juin 2025

Mis à jour le 31 juillet 2025

Créez une référence correcte selon les styles APA, MLA, Chicago, Harvard et plusieurs autres

Choisissez une source :

Consultez les listes thématiques d’articles de revues, de livres, de thèses, de rapports de conférences et d’autres sources académiques sur le sujet « Coq formalization ».

À côté de chaque source dans la liste de références il y a un bouton « Ajouter à la bibliographie ». Cliquez sur ce bouton, et nous générerons automatiquement la référence bibliographique pour la source choisie selon votre style de citation préféré : APA, MLA, Harvard, Vancouver, Chicago, etc.

Vous pouvez aussi télécharger le texte intégral de la publication scolaire au format pdf et consulter son résumé en ligne lorsque ces informations sont inclues dans les métadonnées.

Articles de revues sur le sujet "Coq formalization"

Boender, Jaap, Florian Kammüller, and Rajagopal Nagarajan. "Formalization of Quantum Protocols using Coq." Electronic Proceedings in Theoretical Computer Science 195 (November 4, 2015): 71–83. http://dx.doi.org/10.4204/eptcs.195.6.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Cogumbreiro, Tiago, Jun Shirako, and Vivek Sarkar. "Formalization of Habanero phasers using Coq." Journal of Logical and Algebraic Methods in Programming 90 (August 2017): 50–60. http://dx.doi.org/10.1016/j.jlamp.2017.02.006.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Cogumbreiro, Tiago, Jun Shirako, and Vivek Sarkar. "Formalization of Habanero phasers using Coq." Journal of Logical and Algebraic Methods in Programming 90 (August 1, 2017): 50–60. https://doi.org/10.1016/j.jlamp.2017.02.006.

Texte intégral

Résumé :

Phasers pose an interesting synchronization mechanism that generalizes many collective synchronization patterns seen in parallel programming languages, including barriers, clocks, and point-to-point synchronization using latches or semaphores. This work characterizes scheduling constraints on phaser operations, by relating the execution state of two tasks that operate on the same phaser. We propose a formalization of Habanero phasers, May-Happen-In-Parallel, and Happens-Before relations for phaser operations, and show that these relations conform with the semantics. Our formalization and proof

Styles APA, Harvard, Vancouver, ISO, etc.

Cohen, Joshua M., and Philip Johnson-Freyd. "A Formalization of Core Why3 in Coq." Proceedings of the ACM on Programming Languages 8, POPL (2024): 1789–818. http://dx.doi.org/10.1145/3632902.

Texte intégral

Résumé :

Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools ar

Styles APA, Harvard, Vancouver, ISO, etc.

BOLDO, SYLVIE, CATHERINE LELAY, and GUILLAUME MELQUIOND. "Formalization of real analysis: a survey of proof assistants and libraries." Mathematical Structures in Computer Science 26, no. 7 (2015): 1196–233. http://dx.doi.org/10.1017/s0960129514000437.

Texte intégral

Résumé :

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accoun

Styles APA, Harvard, Vancouver, ISO, etc.

PELAYO, ÁLVARO, VLADIMIR VOEVODSKY, and MICHAEL A. WARREN. "A univalent formalization of the p-adic numbers." Mathematical Structures in Computer Science 25, no. 5 (2015): 1147–71. http://dx.doi.org/10.1017/s0960129514000541.

Texte intégral

Résumé :

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.

Styles APA, Harvard, Vancouver, ISO, etc.

Rauber Du Bois, André, Rodrigo Ribeiro, and Maycon Amaro. "A Mechanized Proof of a Textbook Type Unification Algorithm." Revista de Informática Teórica e Aplicada 27, no. 3 (2020): 13–24. http://dx.doi.org/10.22456/2175-2745.100968.

Texte intégral

Résumé :

Unification is the core of type inference algorithms for modern functional programming languages, like Haskell and SML. As a first step towards a formalization of a type inference algorithm for such programming languages, we present a formalization in Coq of a type unification algorithm that follows classic algorithms presented in programming language textbooks. We also report on the use of such formalization to build a correct type inference algorithm for the simply typed λ-calculus.

Styles APA, Harvard, Vancouver, ISO, etc.

Xu, Yichi, Daniel J. Dougherty, and Rose Bohrer. "A Coq Formalization of Unification Modulo Exclusive-Or." Electronic Proceedings in Theoretical Computer Science 416 (February 11, 2025): 267–73. https://doi.org/10.4204/eptcs.416.23.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

VOEVODSKY, VLADIMIR. "An experimental library of formalized Mathematics based on the univalent foundations." Mathematical Structures in Computer Science 25, no. 5 (2015): 1278–94. http://dx.doi.org/10.1017/s0960129514000577.

Texte intégral

Résumé :

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).

Styles APA, Harvard, Vancouver, ISO, etc.

Fu, Yaoshun, and Wensheng Yu. "Formalizing Calculus without Limit Theory in Coq." Mathematics 9, no. 12 (2021): 1377. http://dx.doi.org/10.3390/math9121377.

Texte intégral

Résumé :

Formal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to found a new form of calculus more easily but rigorously. This theory as an innovation differs from traditional calculus but is equivalent and more comprehensible. First, the definition of the difference-quotient control function is given intuitively from the physical facts. Further, conditions are added

Styles APA, Harvard, Vancouver, ISO, etc.

Plus de sources

Thèses sur le sujet "Coq formalization"

Bartzia, Evmorfia-Iro. "A formalization of elliptic curves for cryptography." Thesis, Université Paris-Saclay (ComUE), 2017. http://www.theses.fr/2017SACLX002/document.

Texte intégral

Résumé :

Le sujet de ma thèse s’inscrit dans le domaine des preuves formelleset de la vérification des algorithmescryptographiques. L’implémentation des algorithmes cryptographiquesest souvent une tâche assez compliquée, parce qu’ils sont optimiséspour être efficaces et sûrs en même temps. Par conséquent, il n’estpas toujours évident qu’un programme cryptographique en tant quefonction, corresponde exactement à l’algorithme mathématique,c’est-à-dire que le programme soit correct. Les erreurs dans lesprogrammes cryptographiques peuvent mettre en danger la sécurité desystèmes cryptographiques entiers et d

Styles APA, Harvard, Vancouver, ISO, etc.

RAMOS, Marcus Vinícius Midena. "Formalization of context-free language theory." Universidade Federal de Pernambuco, 2016. https://repositorio.ufpe.br/handle/123456789/17642.

Texte intégral

Résumé :

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T13:11:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) Made available in DSpace on 2016-08-08T13:11:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) Previous issue date: 2016-03-28 CAPEs Proof assistants are software-based tools that are used in

Styles APA, Harvard, Vancouver, ISO, etc.

Lundstedt, Anders. "Realizability in Coq." Thesis, KTH, Matematik (Avd.), 2015. http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-174109.

Texte intégral

Résumé :

This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinato

Styles APA, Harvard, Vancouver, ISO, etc.

Athalye, Anish (Anish R. ). "CoqIOA : a formalization of IO automata in the Coq proof assistant." Thesis, Massachusetts Institute of Technology, 2017. http://hdl.handle.net/1721.1/112831.

Texte intégral

Résumé :

Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017. This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. Cataloged from student-submitted PDF version of thesis. Includes bibliographical references (pages 51-53). Implementing distributed systems correctly is difficult. Designing correct distributed systems protocols is challenging because designs must account for concurrent operation and handle network and machine failures

Styles APA, Harvard, Vancouver, ISO, etc.

Mouhcine, Houda. "Formal Proofs in Applied Mathematics : A Coq Formalization of Simplicial Lagrange Finite Elements." Electronic Thesis or Diss., université Paris-Saclay, 2024. http://www.theses.fr/2024UPASG112.

Texte intégral

Résumé :

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'appui

Styles APA, Harvard, Vancouver, ISO, etc.

Vinogradova, Polina. "Formalizing Abstract Computability: Turing Categories in Coq." Thesis, Université d'Ottawa / University of Ottawa, 2017. http://hdl.handle.net/10393/36354.

Texte intégral

Résumé :

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more general (abstract) sense. The particular model this thesis is structured around is known as a Turing category. The structure within a Turing category models the notion of partiality as well as recursive computation, and equips us with the tools of category theory to study these concepts. The goal of this work is to build a formal language description of this computation m

Styles APA, Harvard, Vancouver, ISO, etc.

Di, Guardia Rémi. "Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic." Electronic Thesis or Diss., Lyon, École normale supérieure, 2024. http://www.theses.fr/2024ENSL0050.

Texte intégral

Résumé :

Cette thèse s'intéresse à l'égalité des preuves et des formules en logique linéaire, avec des contributions en particulier dans le fragment multiplicatif-additif de cette logique. En logique linéaire, et dans de nombreuses autres logiques (telle que la logique intuitionniste), on dispose de deux transformations sur les preuves : l'élimination des coupures et l'expansion des axiomes. On souhaite très souvent identifier deux preuves reliées par ces transformations, étant donné qu'elles le sont sémantiquement (dans un modèle catégorique par exemple). Cette situation est similaire à celle du λ-cal

Styles APA, Harvard, Vancouver, ISO, etc.

Castro, Cubas Edwars Sleiters, and Pisfil Patricia Nelida Cárdenas. "El incremento patrimonial no justificado y su impacto en la fiscalización tributaria a los youtubers peruanos con más de 100,000 suscriptores de lima 2018." Bachelor's thesis, Universidad Peruana de Ciencias Aplicadas (UPC), 2019. http://hdl.handle.net/10757/652586.

Texte intégral

Résumé :

Hoy en día, el desarrollo tecnológico, permite tener más actividades de servicios realizados por personas naturales, las cuales son gravables con el Impuesto a la Renta e Impuesto General a las Ventas y por ende se requerirá un mayor control por parte de la Administración Tributaria. En estos tiempos de millennials uno de los tantos ingresos que se generan utilizando la tecnología, provienen de los Youtubers, quienes por su falta de conocimiento de sus obligaciones tributarias y/o falta conciencia tributaria, incide en que incumplan con el pago de sus impuestos. Dichas omisiones ocasionan una

Styles APA, Harvard, Vancouver, ISO, etc.

Livres sur le sujet "Coq formalization"

Guidance on leveraging sustainability pathways to accelerate formalization. ILO, 2024. http://dx.doi.org/10.54394/00000015.

Texte intégral

Résumé :

This guidance note has been developed through the ongoing collaboration between the Federation of Egyptian Industries (FEI) and the International Labour Organization (ILO) within the framework of the regional project, "Social Dialogue for Formalization and Employability in the Southern Neighbourhood (SOLIFEM)," which is being implemented by the ILO and co-financed by the European Union in Egypt, among the four focus countries of the project (Algeria, Lebanon & Occupied Palestinian Territories). The primary objective of this guidance note is to show the relationship between corporate sustai

Styles APA, Harvard, Vancouver, ISO, etc.

Chapitres de livres sur le sujet "Coq formalization"

Gallois-Wong, Diane, Sylvie Boldo, and Thibault Hilaire. "A Coq Formalization of Digital Filters." In Lecture Notes in Computer Science. Springer International Publishing, 2018. http://dx.doi.org/10.1007/978-3-319-96812-4_8.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Cohen, Cyril, and Anders Mörtberg. "A Coq Formalization of Finitely Presented Modules." In Interactive Theorem Proving. Springer International Publishing, 2014. http://dx.doi.org/10.1007/978-3-319-08970-6_13.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Tsai, Ming-Hsien, and Bow-Yaw Wang. "Modular Formalization of Reactive Modules in COQ." In Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. Springer Berlin Heidelberg, 2007. http://dx.doi.org/10.1007/978-3-540-77505-8_9.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Génevaux, Jean-David, Julien Narboux, and Pascal Schreck. "Formalization of Wu’s Simple Method in Coq." In Certified Programs and Proofs. Springer Berlin Heidelberg, 2011. http://dx.doi.org/10.1007/978-3-642-25379-9_8.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Yan, Sheng, Yaoshun Fu, Dakai Guo, and Wensheng Yu. "A Formalization of Topological Spaces in Coq." In Proceeding of 2021 International Conference on Wireless Communications, Networking and Applications. Springer Nature Singapore, 2022. http://dx.doi.org/10.1007/978-981-19-2456-9_21.

Texte intégral

Résumé :

AbstractIt is a wish for Wu Wen-tsun to implement the mechanical proving of theorems in topology. Topological spaces constitute a fundamental concept of general topology, which is significant in understanding the essential content of general topology. Based on the machine proof system of axiomatic set theory, we presented a computer formalization of topological spaces in Coq. Basic examples of topological spaces are formalized, including indiscrete topological spaces and discrete topological spaces. Furthermore, the formal description of some well-known equivalent definitions of topological sp

Styles APA, Harvard, Vancouver, ISO, etc.

Affeldt, Reynald, and Manabu Hagiwara. "Formalization of Shannon’s Theorems in SSReflect-Coq." In Interactive Theorem Proving. Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-32347-8_16.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Benzaken, Véronique, Évelyne Contejean, and Stefania Dumbrava. "A Coq Formalization of the Relational Data Model." In Programming Languages and Systems. Springer Berlin Heidelberg, 2014. http://dx.doi.org/10.1007/978-3-642-54833-8_11.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Affeldt, Reynald, and Naoki Kobayashi. "Formalization and Verification of a Mail Server in Coq." In Software Security — Theories and Systems. Springer Berlin Heidelberg, 2003. http://dx.doi.org/10.1007/3-540-36532-x_14.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Dou, Guowei, and Wensheng Yu. "Formalization of the Filter Extension Principle (FEP) in Coq." In Communications in Computer and Information Science. Springer Nature Singapore, 2024. http://dx.doi.org/10.1007/978-981-97-3951-6_10.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Guo, Dakai, Shukun Leng, Si Chen, and Wensheng Yu. "Lagrange’s Theorem in Group Theory: Formalization and Proof with Coq." In Communications in Computer and Information Science. Springer Nature Singapore, 2024. http://dx.doi.org/10.1007/978-981-97-3951-6_11.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Actes de conférences sur le sujet "Coq formalization"

Yu, Liumiao, Yan Chen, and Wensheng Yu. "Formalization of the Cauchy Convergence Criterion for Sequences in Coq." In 2024 China Automation Congress (CAC). IEEE, 2024. https://doi.org/10.1109/cac63892.2024.10864519.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Wang, Yifei, and Gang Chen. "Formalization of Laplace Transform in Coq." In 2017 International Conference on Dependable Systems and Their Applications (DSA). IEEE, 2017. http://dx.doi.org/10.1109/dsa.2017.12.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Benzaken, Véronique, Sarah Cohen-Boulakia, Évelyne Contejean, Chantal Keller, and Rébecca Zucchini. "A Coq formalization of data provenance." In CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, 2021. http://dx.doi.org/10.1145/3437992.3439920.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Sun, Tianyu, Wensheng Yu, and Yaoshun Fu. "Formalization of Transfinite Induction in Coq*." In 2019 Chinese Automation Congress (CAC). IEEE, 2019. http://dx.doi.org/10.1109/cac48633.2019.8997376.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Leng, Shukun, Dakai Guo, and Wensheng Yu. "Formalization of Dedekind Fundamental Theorem in Coq." In 2023 China Automation Congress (CAC). IEEE, 2023. http://dx.doi.org/10.1109/cac59555.2023.10450761.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Wan, Hai, Gang Chen, Xiaoyu Song, and Ming Gu. "Formalization and Verification of PLC Timers in Coq." In 2009 33rd Annual IEEE International Computer Software and Applications Conference. IEEE, 2009. http://dx.doi.org/10.1109/compsac.2009.49.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Philippe, Jolan, Wadoud Bousdira, and Frederic Loulergue. "Formalization of a Big Graph API in Coq." In 2017 International Conference on High Performance Computing & Simulation (HPCS). IEEE, 2017. http://dx.doi.org/10.1109/hpcs.2017.140.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Bauer, Andrej, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. "The HoTT library: a formalization of homotopy type theory in Coq." In CPP '17: Certified Proofs and Programs. ACM, 2017. http://dx.doi.org/10.1145/3018610.3018615.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Wieczorek, Paweł, and Dariusz Biernacki. "A Coq formalization of normalization by evaluation for Martin-Löf type theory." In CPP '18: Certified Proofs and Programs. ACM, 2018. http://dx.doi.org/10.1145/3167091.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Wieczorek, Paweł, and Dariusz Biernacki. "A Coq formalization of normalization by evaluation for Martin-Löf type theory." In the 7th ACM SIGPLAN International Conference. ACM Press, 2018. http://dx.doi.org/10.1145/3176245.3167091.

Texte intégral

Styles APA, Harvard, Vancouver, ISO, etc.

Nous offrons des réductions sur tous les plans premium pour les auteurs dont les œuvres sont incluses dans des sélections littéraires thématiques. Contactez-nous pour obtenir un code promo unique!