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

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

1 2 3 ... 90 91 92 next

  1. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  2. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  3. Berger, Ulrich; Tsuiki, Hideki: Intuitionistic fixed point logic (2021)
  4. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  5. Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
  6. Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
  7. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  8. Pattinson, Dirk; Mohammadian, Mina: Constructive domains with classical witnesses (2021)
  9. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  10. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  11. Steinberg, Florian; Thery, Laurent; Thies, Holger: Computable analysis and notions of continuity in \textscCoq (2021)
  12. Veltri, Niccolò; van der Weide, Niels: Constructing higher inductive types as groupoid quotients (2021)
  13. Xie, Wanling; Zhu, Huibiao; Xu, Qiwen: A process calculus BigrTiMo of mobile systems and its formal semantics (2021)
  14. 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)
  15. Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi: A library for formalization of linear error-correcting codes (2020)
  16. Affeldt, Reynald; Garrigue, Jacques; Saikawa, Takafumi: Formal adventures in convex and conical spaces (2020)
  17. Albert, Elvira; Bezirgiannis, Nikolaos; De Boer, Frank; Martin-Martin, Enrique: A formal, resource consumption-preserving translation from actors with cooperative scheduling to Haskell (2020)
  18. Andrade Guzmán, Jesús Mauricio; Hernández Quiroz, Francisco: Natural deduction and semantic models of justification logic in the proof assistant \textscCoq (2020)
  19. Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
  20. Bana, Gergei; Chadha, Rohit; Eeralla, Ajay Kumar; Okada, Mitsuhiro: Verification methods for the computationally complete symbolic attacker based on indistinguishability (2020)

1 2 3 ... 90 91 92 next