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

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

1 2 3 ... 83 84 85 next

  1. Ahrens, Benedikt; Lefanu Lumsdaine, Peter: Displayed categories (2019)
  2. Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders: From signatures to Monads in \textsfUniMath (2019)
  3. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2019)
  4. Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele: A formalisation of nominal C-matching through unification with protected variables (2019)
  5. 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)
  6. Balabonski, Thibaut; Delga, Amélie; Rieg, Lionel; Tixeuil, Sébastien; Urbain, Xavier: Synchronous gathering without multiplicity detection: a certified algorithm (2019)
  7. Bana, Gergei; Chadha, Rohit; Eeralla, Ajay Kumar; Okada, Mitsuhiro: Verification methods for the computationally complete symbolic attacker based on indistinguishability (2019)
  8. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)
  9. Beeson, Michael; Narboux, Julien; Wiedijk, Freek: Proof-checking Euclid (2019)
  10. Bendkowski, Maciej; Bodini, Olivier; Dovgal, Sergey: Statistical properties of lambda terms (2019)
  11. Biernacki, Dariusz; Lenglet, Serguei; Polesiuk, Piotr: Proving soundness of extensional normal-form bisimilarities (2019)
  12. Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea: Guarded cubical type theory (2019)
  13. Boulmé, Sylvain; Maréchal, Alexandre: Refinement to certify abstract interpretations: illustrated on linearization for polyhedra (2019)
  14. Boutry, Pierre; Braun, Gabriel; Narboux, Julien: Formalization of the arithmetization of Euclidean plane geometry and applications (2019)
  15. Boutry, Pierre; Gries, Charly; Narboux, Julien; Schreck, Pascal: Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq (2019)
  16. Braun, David; Magaud, Nicolas; Schreck, Pascal: Two cryptomorphic formalizations of projective incidence geometry (2019)
  17. Chan, Hing-Lun; Norrish, Michael: Classification of finite fields with applications (2019)
  18. Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
  19. Cruz-Filipe, Luís; Marques-Silva, Joao; Schneider-Kamp, Peter: Formally verifying the solution to the Boolean Pythagorean triples problem (2019)
  20. Dabrowski, Frédéric: A denotational semantics of textually aligned SPMD programs (2019)

1 2 3 ... 83 84 85 next