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

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

1 2 3 ... 66 67 68 next

  1. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  2. Biernacki, Dariusz; Polesiuk, Piotr: Logical relations for coherence of effect subtyping (2018)
  3. Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (2018)
  4. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  5. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  6. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)
  7. Paviotti, Marco; Bengtson, Jesper: Formally verifying exceptions for low-level code with separation logic (2018)
  8. Tan, Gang; Morrisett, Greg: Bidirectional grammars for machine-code decoding and encoding (2018)
  9. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2017)
  10. Alpuim, João; Oliveira, Bruno C.d.S.; Shi, Zhiyuan: Disjoint polymorphism (2017)
  11. Altisen, Karine; Corbineau, Pierre; Devismes, Stephane: A framework for certified self-stabilization (2017)
  12. Amin, Nada; Rompf, Tiark: Type soundness proofs with definitional interpreters (2017)
  13. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal $\alpha$-equivalence with A and AC function symbols (2017)
  14. Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)
  15. Bagnall, Alexander; Merten, Samuel; Stewart, Gordon: Brief announcement: Certified multiplicative weights update: verified learning without regret (2017)
  16. Benzaken, Véronique; Contejean, Évelyne; Dumbrava, Stefania: Certifying standard and stratified Datalog inference engines in SSReflect (2017)
  17. Bernard, Sophie: Formalization of the Lindemann-Weierstrass theorem (2017)
  18. Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre: Compcerts: a memory-aware verified C compiler using pointer as integer semantics (2017)
  19. Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy: Friends with benefits. Implementing corecursion in foundational proof assistants (2017)
  20. Boldo, Sylvie; Joldes, Mioara; Muller, Jean-Michel; Popescu, Valentina: Formal verification of a floating-point expansion renormalization algorithm (2017)

1 2 3 ... 66 67 68 next