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

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

1 2 3 ... 73 74 75 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. Ahrens, Benedikt; Lefanu Lumsdaine, Peter: Displayed categories (2019)
  3. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele; Rocha-Oliveira, Ana Cristina: A formalisation of nominal (\alpha)-equivalence with A, C, and AC function symbols (2019)
  4. Biernacki, Dariusz; Lenglet, Serguei; Polesiuk, Piotr: Proving soundness of extensional normal-form bisimilarities (2019)
  5. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
  6. Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (2019)
  7. Braun, David; Magaud, Nicolas; Schreck, Pascal: Two cryptomorphic formalizations of projective incidence geometry (2019)
  8. Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
  9. Dagnino, Francesco: Coaxioms: flexible coinductive definitions by inference systems (2019)
  10. de Gouw, Stijn; de Boer, Frank S.; Bubel, Richard; Hähnle, Reiner; Rot, Jurriaan; Steinhöfel, Dominic: Verifying OpenJDK’s sort method for generic collections (2019)
  11. Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
  12. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  13. Grégoire, Thomas; Chlipala, Adam: Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms (2019)
  14. Haraway, Robert C. III: Practical bounds for a Dehn parental test (2019)
  15. Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
  16. Jay, Barry: Intensional computation with higher-order functions (2019)
  17. Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas: Formally verified approximations of definite integrals (2019)
  18. Marić, Filip: Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (2019)
  19. Nipkow, Tobias; Brinkop, Hauke: Amortized complexity verified (2019)
  20. Ştefănescu, Andrei; Ciob^acă, Stefan; Mereuta, Radu; Moore, Brandon; Roşu, Grigore; Şerbănuṭă, Traian Florin: All-path reachability logic (2019)

1 2 3 ... 73 74 75 next