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

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

1 2 3 ... 70 71 72 next

  1. Magron, Victor; Safey El Din, Mohab; Schweighofer, Markus: Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials (2019-2019)
  2. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
  3. Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (2019)
  4. Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
  5. Dagnino, Francesco: Coaxioms: flexible coinductive definitions by inference systems (2019)
  6. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  7. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  8. Haraway, Robert C. III: Practical bounds for a Dehn parental test (2019)
  9. Jay, Barry: Intensional computation with higher-order functions (2019)
  10. Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir: Categorical structures for type theory in univalent foundations (2018)
  11. Ahrens, Benedikt; Matthes, Ralph: Heterogeneous substitution systems revisited (2018)
  12. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  13. Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas: Towards certified meta-programming with typed Template-Coq (2018)
  14. Angiuli, Carlo; Harper, Robert: Meaning explanations at higher dimension (2018)
  15. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: Nominal C-unification (2018)
  16. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
  17. Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of (\pi): formal proofs of some algorithms computing them and guarantees of exact computation (2018)
  18. Biernacki, Dariusz; Polesiuk, Piotr: Logical relations for coherence of effect subtyping (2018)
  19. Bonifati, Angela; Dumbrava, Stefania; Arias, Emilio Jesús Gallego: Certified graph view maintenance with regular Datalog (2018)
  20. Cao, Qinxiang; Beringer, Lennart; Gruetter, Samuel; Dodds, Josiah; Appel, Andrew W.: VST-Floyd: a separation logic tool to verify correctness of C programs (2018)

1 2 3 ... 70 71 72 next