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

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

1 2 3 ... 67 68 69 next

  1. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019-2019)
  2. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019-2019)
  3. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  4. Biernacki, Dariusz; Polesiuk, Piotr: Logical relations for coherence of effect subtyping (2018)
  5. Clochard, Martin; Gondelman, Léon; Pereira, Mário: The matrix reproved (verification pearl) (2018)
  6. Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
  7. de Putter, Sander; Wijs, Anton: A formal verification technique for behavioural model-to-model transformations (2018)
  8. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  9. Genet, Thomas; Haudebourg, Timothée; Jensen, Thomas: Verifying higher-order functions with tree automata (2018)
  10. He, Shaobo; Lahiri, Shuvendu K.; Rakamarić, Zvonimir: Verifying relative safety, accuracy, and termination for program approximations (2018)
  11. Léchenet, Jean-Christophe; Kosmatov, Nikolai; Le Gall, Pascale: Cut branches before looking for bugs: certifiably sound verification on relaxed slices (2018)
  12. Mizuno, Masayuki; Sumii, Eijiro: Formal verification of the correspondence between call-by-need and call-by-name (2018)
  13. Paviotti, Marco; Bengtson, Jesper: Formally verifying exceptions for low-level code with separation logic (2018)
  14. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  15. Sakaguchi, Kazuhiko: Program extraction for mutable arrays (2018)
  16. Stump, Aaron: From realizability to induction via dependent intersection (2018)
  17. Tan, Gang; Morrisett, Greg: Bidirectional grammars for machine-code decoding and encoding (2018)
  18. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2017)
  19. Alpuim, João; Oliveira, Bruno C.d. S.; Shi, Zhiyuan: Disjoint polymorphism (2017)
  20. Altisen, Karine; Corbineau, Pierre; Devismes, Stephane: A framework for certified self-stabilization (2017)

1 2 3 ... 67 68 69 next