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

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

1 2 3 ... 90 91 92 next

  1. Ahrens, Benedikt; Hirschowitz, André; Lafont, Ambroise; Maggesi, Marco: Presentable signatures and initial semantics (2021)
  2. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  3. Arusoaie, Andrei: Certifying Findel derivatives for blockchain (2021)
  4. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  5. Berger, Ulrich; Tsuiki, Hideki: Intuitionistic fixed point logic (2021)
  6. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  7. Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
  8. Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
  9. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  10. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  11. Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
  12. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  13. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  14. Pattinson, Dirk; Mohammadian, Mina: Constructive domains with classical witnesses (2021)
  15. Reed Oei, Dun Ma, Christian Schulz, Philipp Hieronymi: Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata (2021) arXiv
  16. Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
  17. Steinberg, Florian; Thery, Laurent; Thies, Holger: Computable analysis and notions of continuity in \textscCoq (2021)
  18. Veltri, Niccolò; van der Weide, Niels: Constructing higher inductive types as groupoid quotients (2021)
  19. Xie, Wanling; Zhu, Huibiao; Xu, Qiwen: A process calculus BigrTiMo of mobile systems and its formal semantics (2021)
  20. 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)

1 2 3 ... 90 91 92 next