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

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

1 2 3 ... 94 95 96 next

  1. Boldo, Sylvie; Clément, François; Faissole, Florian; Martin, Vincent; Mayero, Micaela: A Coq formalization of Lebesgue integration of nonnegative functions (2022)
  2. Bordg, Anthony; Paulson, Lawrence; Li, Wenda: Simple type theory is not too simple: Grothendieck’s schemes without dependent types (2022)
  3. Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
  4. Forster, Yannick: Parametric Church’s thesis: synthetic computability without choice (2022)
  5. Hagemeier, Christian; Kirst, Dominik: Constructive and mechanised meta-theory of intuitionistic epistemic logic (2022)
  6. Hirata, Michikazu; Minamide, Yasuhiko; Sato, Tetsuya: Program logic for higher-order probabilistic programs in Isabelle/HOL (2022)
  7. Kastberg Hinrichsen, Jonas; Bengtson, Jesper; Krebbers, Robbert: \textbfActris2.0: asynchronous session-type based reasoning in separation logic (2022)
  8. Kirst, Dominik; Larchey-Wendling, Dominique: Trakhtenbrot’s theorem in Coq: finite model theory through the constructive lens (2022)
  9. Krijnen, Jacco O. G.; Chakravarty, Manuel M. T.; Keller, Gabriele; Swierstra, Wouter: Translation certification for smart contracts (2022)
  10. Larchey-Wendling, Dominique; Forster, Yannick: Hilbert’s tenth problem in Coq (extended version) (2022)
  11. Larchey-Wendling, Dominique; Monin, Jean-François: The Braga method: extracting certified algorithms from complex recursive schemes in Coq (2022)
  12. Lewis, Robert Y.; Wu, Minchao: A bi-directional extensible interface between Lean and Mathematica (2022)
  13. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  14. Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi: A trustful monad for axiomatic reasoning with probability and nondeterminism (2021)
  15. Ahrens, Benedikt; Hirschowitz, André; Lafont, Ambroise; Maggesi, Marco: Presentable signatures and initial semantics (2021)
  16. Ambal, Guillaume; Lenglet, Sergueï; Schmitt, Alan: (\mathrmHO\pi) in Coq (2021)
  17. Arusoaie, Andrei: Certifying Findel derivatives for blockchain (2021)
  18. Ayala-Rincón, Mauricio; De Carvalho-Segundo, Washington; Fernández, Maribel; Silva, Gabriel Ferreira; Nantes-Sobrinho, Daniele: Formalising nominal C-unification generalised with protected variables (2021)
  19. Bartoletti, Massimo; Bracciali, Andrea; Lepore, Cristian; Scalas, Alceste; Zunino, Roberto: A formal model of Algorand smart contracts (2021)
  20. Bentkamp, Alexander; Blanchette, Jasmin; Cruanes, Simon; Waldmann, Uwe: Superposition for lambda-free higher-order logic (2021)

1 2 3 ... 94 95 96 next