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

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

1 2 3 ... 86 87 88 next

  1. Bana, Gergei; Chadha, Rohit; Eeralla, Ajay Kumar; Okada, Mitsuhiro: Verification methods for the computationally complete symbolic attacker based on indistinguishability (2020)
  2. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  3. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  4. Czajka, Łukasz: A new coinductive confluence proof for infinitary lambda calculus (2020)
  5. Forster, Yannick; Kirst, Dominik; Wehr, Dominik: Completeness theorems for first-order logic analysed in constructive type theory (2020)
  6. Ishii, Daisuke; Yabu, Tomohito: Computer-assisted verification of four interval arithmetic operators (2020)
  7. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  8. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  9. Li, Wenda; Paulson, Lawrence C.: Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL (2020)
  10. Peña, Ricardo: An assertional proof of red-black trees using Dafny (2020)
  11. Affeldt, Reynald; Nowak, David; Saikawa, Takafumi: A hierarchy of monadic effects for program verification using equational reasoning (2019)
  12. Ahrens, Benedikt; Lefanu Lumsdaine, Peter: Displayed categories (2019)
  13. Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders: From signatures to Monads in \textsfUniMath (2019)
  14. Alessi, Fabio; Ciaffaglione, Alberto; Di Gianantonio, Pietro; Honsell, Furio; Lenisa, Marina; Scagnetto, Ivan: (\mathrmLF^+) in \textttCoqfor fast-and-loose reasoning (2019)
  15. Allamigeon, Xavier; Katz, Ricardo D.: A formalization of convex polyhedra based on the simplex method (2019)
  16. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  17. 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)
  18. 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)
  19. Balabonski, Thibaut; Delga, Amélie; Rieg, Lionel; Tixeuil, Sébastien; Urbain, Xavier: Synchronous gathering without multiplicity detection: a certified algorithm (2019)
  20. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)

1 2 3 ... 86 87 88 next