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

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

1 2 3 ... 56 57 58 next

  1. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  2. Braun, Gabriel; Narboux, Julien: A synthetic proof of Pappus’ theorem in Tarski’s geometry (2017)
  3. Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
  4. Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
  5. Cogumbreiro, Tiago; Shirako, Jun; Sarkar, Vivek: Formalization of Habanero phasers using Coq (2017)
  6. Doko, Marko; Vafeiadis, Viktor: Tackling real-life relaxed concurrency with FSL++ (2017)
  7. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: Lincx: a linear logical framework with first-class contexts (2017)
  8. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  9. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  10. Krebbers, Robbert; Jung, Ralf; Bizjak, Aleš; Jourdan, Jacques-Henri; Dreyer, Derek; Birkedal, Lars: The essence of higher-order concurrent separation logic (2017)
  11. Maietti, Maria Emilia: On choice rules in dependent type theory (2017)
  12. Renac, Florent: A robust high-order Lagrange-projection like scheme with large time steps for the isentropic Euler equations (2017)
  13. Renac, Florent: A robust high-order discontinuous Galerkin method with large time steps for the compressible Euler equations (2017)
  14. Schäfer, Steven; Smolka, Gert: Tower induction and up-to techniques for CCS with fixed points (2017)
  15. Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
  16. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  17. Stucke, Insa: Reasoning about cardinalities of relations with applications supported by proof assistants (2017)
  18. Tassarotti, Joseph; Jung, Ralf; Harper, Robert: A higher-order logic for concurrent termination-preserving refinement (2017)
  19. van Hulst, A.C.; Reniers, M.A.; Fokkink, W.J.: Maximally permissive controlled system synthesis for non-determinism and modal logic (2017)
  20. Zeljić, Aleksandar; Wintersteiger, Christoph M.; Rümmer, Philipp: An approximation framework for solvers and decision procedures (2017)

1 2 3 ... 56 57 58 next