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

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

1 2 3 ... 54 55 56 next

  1. Renac, Florent: A robust high-order Lagrange-projection like scheme with large time steps for the isentropic Euler equations (2017)
  2. Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
  3. van Hulst, A.C.; Reniers, M.A.; Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic (2017)
  4. Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)
  5. Altisen, Karine; Corbineau, Pierre; Devismes, Stéphane: A framework for certified self-stabilization (2016)
  6. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  7. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  8. Blazy, Sandrine; Laporte, Vincent; Pichardie, David: Verified abstract interpretation techniques for disassembling low-level self-modifying code (2016)
  9. Brunet, Paul; Pous, Damien; Stucke, Insa: Cardinalities of finite relations in Coq (2016)
  10. Buchberger, Bruno: The GDML and eukim projects: short report on the initiative (2016)
  11. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  12. Ciob^acă, Ştefan; Lucanu, Dorel; Rusu, Vlad; Roşu, Grigore: A language-independent proof system for full program equivalence (2016)
  13. Coghetto, Roland: Homography in $\mathbbR\mathbbP^2$ (2016)
  14. Coghetto, Roland; Grabowski, Adam: Tarski geometry axioms. II (2016)
  15. Derouet-Jourdan, Alexandre; Mizoguchi, Yoshihiro; Salvati, Marc: Wang tile modeling of wall patterns (2016)
  16. Doczkal, Christian; Smolka, Gert: Completeness and decidability results for CTL in constructive type theory (2016)
  17. Doczkal, Christian; Smolka, Gert: Two-way automata in Coq (2016)
  18. Doko, Marko; Vafeiadis, Viktor: A program logic for C11 memory fences (2016)
  19. Dubois, Catherine; Giorgetti, Alain; Genestier, Richard: Tests and proofs for enumerative combinatorics (2016)
  20. Dubois, Catherine; Pessaux, François: Termination proofs for recursive functions in FoCaLiZe (2016)

1 2 3 ... 54 55 56 next