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

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

1 2 3 ... 55 56 57 next

  1. Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)
  2. Bernardeschi, Cinzia; Domenici, Andrea: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system (2016)
  3. Blanqui, Frédéric: Termination of rewrite relations on $\lambda$-terms based on Girard’s notion of reducibility (2016)
  4. Blazy, Sandrine; Laporte, Vincent; Pichardie, David: Verified abstract interpretation techniques for disassembling low-level self-modifying code (2016)
  5. Buchberger, Bruno: The GDML and eukim projects: short report on the initiative (2016)
  6. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  7. Doczkal, Christian; Smolka, Gert: Completeness and decidability results for CTL in constructive type theory (2016)
  8. Doko, Marko; Vafeiadis, Viktor: A program logic for C11 memory fences (2016)
  9. Dubois, Catherine; Pessaux, François: Termination proofs for recursive functions in FoCaLiZe (2016)
  10. Goto, Matthew; Jagadeesan, Radha; Jeffrey, Alan; Pitcher, Corin; Riely, James: An extensible approach to session polymorphism (2016)
  11. Joldes, Mioara; Muller, Jean-Michel; Popescu, Valentina; Tucker, Warwick: CAMPARY: cuda multiple precision arithmetic library and applications (2016)
  12. Katis, Andreas; Gacek, Andrew; Whalen, Michael W.: Machine-checked proofs for realizability checking algorithms (2016)
  13. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  14. Larchey-Wendling, Dominique: The formal strong completeness of partial monoidal Boolean BI (2016)
  15. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: sound verification on relaxed slices (2016)
  16. McCarthy, Jay; Fetscher, Burke; New, Max; Feltey, Daniel; Findler, Robert Bruce: A Coq library for internal verification of running-times (2016)
  17. Narboux, Julien; Braun, David: Towards a certified version of the encyclopedia of triangle centers (2016)
  18. Rabe, Florian: The future of logic: foundation-independence (2016)
  19. Rahli, Vincent: Exercising Nuprl’s open-endedness (2016)
  20. Ramos, Marcus Vinícius Midena; de Queiroz, Ruy J.G.B.; Moreira, Nelma; Almeida, José Carlos Bacelar: On the formalization of some results of context-free language theory (2016)

1 2 3 ... 55 56 57 next