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 1784 articles , 3 standard articles )

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

1 2 3 ... 88 89 90 next

  1. 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)
  2. Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi: A library for formalization of linear error-correcting codes (2020)
  3. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  4. Bana, Gergei; Chadha, Rohit; Eeralla, Ajay Kumar; Okada, Mitsuhiro: Verification methods for the computationally complete symbolic attacker based on indistinguishability (2020)
  5. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  6. Bizjak, Aleš; Ejlers Møgelberg, Rasmus: Denotational semantics for guarded dependent type theory (2020)
  7. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  8. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  9. Czajka, Łukasz: A new coinductive confluence proof for infinitary lambda calculus (2020)
  10. Doczkal, Christian; Pous, Damien: Graph theory in Coq: minors, treewidth, and isomorphisms (2020)
  11. Ekici, Burak; Kaliszyk, Cezary: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq (2020)
  12. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Mechanizing bisimulation theorems for relation-changing logics in Coq (2020)
  13. Forster, Yannick; Kirst, Dominik; Wehr, Dominik: Completeness theorems for first-order logic analysed in constructive type theory (2020)
  14. Ishii, Daisuke; Yabu, Tomohito: Computer-assisted verification of four interval arithmetic operators (2020)
  15. Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
  16. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  17. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  18. Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
  19. Miranda-Perea, Favio E.; González Huesca, Lourdes del Carmen; Linares-Arévalo, P. Selene: Interactive proof-search for equational reasoning (2020)
  20. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)

1 2 3 ... 88 89 90 next