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

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

1 2 3 ... 91 92 93 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi: A trustful monad for axiomatic reasoning with probability and nondeterminism (2021)
  3. Ahrens, Benedikt; Hirschowitz, André; Lafont, Ambroise; Maggesi, Marco: Presentable signatures and initial semantics (2021)
  4. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  5. Arusoaie, Andrei: Certifying Findel derivatives for blockchain (2021)
  6. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)
  7. Berger, Ulrich; Tsuiki, Hideki: Intuitionistic fixed point logic (2021)
  8. Beringer, Lennart: Verified software units (2021)
  9. Booij, Auke B.: Extensional constructive real analysis via locators (2021)
  10. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  11. Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben: Safe functional systems through integrity types and verified assembly (2021)
  12. Cristiá, Maximiliano; Rossi, Gianfranco: Automated proof of Bell-LaPadula security properties (2021)
  13. Emmenegger, Jacopo: W-types in setoids (2021)
  14. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  15. Frumin, Dan; Krebbers, Robbert; Birkedal, Lars: ReLoC reloaded: a mechanized relational logic for fine-grained concurrency and logical atomicity (2021)
  16. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  17. Hötzel Escardó, Martín: Injective types in univalent mathematics (2021)
  18. Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume: Modular verification of programs with effects and effects handlers (2021)
  19. Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
  20. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)

1 2 3 ... 91 92 93 next