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

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

1 2 3 ... 60 61 62 next

  1. Alpuim, João; Oliveira, Bruno C.d.S.; Shi, Zhiyuan: Disjoint polymorphism (2017)
  2. Amin, Nada; Rompf, Tiark: Type soundness proofs with definitional interpreters (2017)
  3. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  4. Boldo, Sylvie; Melquiond, Guillaume: Computer arithmetic and formal proofs. Floating-point algorithms with the Coq system (to appear) (2017)
  5. Braun, Gabriel; Narboux, Julien: A synthetic proof of Pappus’ theorem in Tarski’s geometry (2017)
  6. Carter, Nathan C.; Monks, Kenneth G.: A web-based toolkit for mathematical word processing applications with semantics (2017)
  7. Charguéraud, Arthur; Pottier, François: Temporary Read-only permissions for separation logic (2017)
  8. Chiang, Wei-Fan; Baranowski, Mark; Briggs, Ian; Solovyev, Alexey; Gopalakrishnan, Ganesh; Rakamarić, Zvonimir: Rigorous floating-point mixed-precision tuning (2017)
  9. Chojecki, Przemysław: Deepalgebra -- an outline of a program (2017)
  10. Cogumbreiro, Tiago; Shirako, Jun; Sarkar, Vivek: Formalization of Habanero phasers using Coq (2017)
  11. Crary, Karl: Modules, abstraction, and parametric polymorphism (2017)
  12. Cruz-Filipe, Luís; Heule, Marijn J.H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  13. Doko, Marko; Vafeiadis, Viktor: Tackling real-life relaxed concurrency with FSL++ (2017)
  14. Georges, Aina Linn; Murawska, Agata; Otis, Shawn; Pientka, Brigitte: Lincx: a linear logical framework with first-class contexts (2017)
  15. Glück, Roland: Algebraic investigation of connected components (2017)
  16. Ilik, Danko: The exp-log normal form of types: decomposing extensional equality and representing terms compactly (2017)
  17. Kanckos, Annika; Woltzenlogel Paleo, B.: Variants of Gödel’s ontological proof in a natural deduction calculus (2017)
  18. Kang, Jeehoon; Hur, Chung-Kil; Lahav, Ori; Vafeiadis, Viktor; Dreyer, Derek: A promising semantics for relaxed-memory concurrency (2017)
  19. Kojima, Kensuke; Igarashi, Atsushi: A Hoare logic for GPU kernels (2017)
  20. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)

1 2 3 ... 60 61 62 next