Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.


References in zbMATH (referenced in 1799 articles , 3 standard articles )

Showing results 1 to 20 of 1799.
Sorted by year (citations)

1 2 3 ... 88 89 90 next

  1. Berger, Ulrich; Tsuiki, Hideki: Intuitionistic fixed point logic (2021)
  2. Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
  3. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  4. Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam: Proof-producing synthesis of CakeML from monadic HOL functions (2020)
  5. Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi: A library for formalization of linear error-correcting codes (2020)
  6. Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi: Formal adventures in convex and conical spaces (2020)
  7. Andrade Guzmán, Jesús Mauricio; Hernández Quiroz, Francisco: Natural deduction and semantic models of justification logic in the proof assistant \textscCoq (2020)
  8. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  9. Bana, Gergei; Chadha, Rohit; Eeralla, Ajay Kumar; Okada, Mitsuhiro: Verification methods for the computationally complete symbolic attacker based on indistinguishability (2020)
  10. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David: System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (2020)
  11. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  12. Bizjak, Aleš; Ejlers Møgelberg, Rasmus: Denotational semantics for guarded dependent type theory (2020)
  13. Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman: The Tactician. A seamless, interactive tactic learner and prover for Coq (2020)
  14. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  15. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  16. Czajka, Łukasz: A new coinductive confluence proof for infinitary lambda calculus (2020)
  17. del Carmen González Huesca, Lourdes; Miranda Perea, Favio Ezequiel; Linares-Arévalo, P. Selene: Dual and axiomatic systems for constructive S4, a formally verified equivalence (2020)
  18. Doczkal, Christian; Pous, Damien: Graph theory in Coq: minors, treewidth, and isomorphisms (2020)
  19. Ekici, Burak; Kaliszyk, Cezary: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq (2020)
  20. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Mechanizing bisimulation theorems for relation-changing logics in Coq (2020)

1 2 3 ... 88 89 90 next