Coq/SSReflect

Ssreflect extension library for the Coq proof assistant. The name Ssreflect stands for ”small scale reflection”, a style of proof that evolved from the computer-checked proof of the Four Colour Theorem and which leverages the higher-order nature of Coq’s underlying logic to provide effective automation for many small, clerical proof steps. This is often accomplished by restating (”reflecting”) problems in a more concrete form, hence the name. For example, in the Ssreflect library arithmetic comparison is not an abstract predicate, but a function computing a boolean.


References in zbMATH (referenced in 42 articles )

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

1 2 3 next

  1. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  2. Doczkal, Christian; Smolka, Gert: Completeness and decidability results for CTL in constructive type theory (2016)
  3. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  4. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  5. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  6. Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent: Formally verified certificate checkers for hardest-to-round computation (2015)
  7. Affeldt, Reynald; Hagiwara, Manabu; Sénizergues, Jonas: Formalization of Shannon’s theorems (2014)
  8. Aransay, Jesús; Divasón, Jose: Formalization and execution of linear algebra: from theorems to algorithms (2014)
  9. Bartzia, Evmorfia-Iro; Strub, Pierre-Yves: A formal library for elliptic curves in the Coq proof assistant (2014)
  10. Cohen, Cyril; Mörtberg, Anders: A Coq formalization of finitely presented modules (2014)
  11. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  12. Poza, María; Domínguez, César; Heras, Jónathan; Rubio, Julio: A certified reduction strategy for homological image processing (2014)
  13. Zsidó, Julianna: Theorem of three circles in Coq (2014)
  14. Doczkal, Christian; Kaiser, Jan-Oliver; Smolka, Gert: A constructive theory of regular languages in Coq (2013)
  15. Gonthier, Georges: Engineering mathematics: the odd order theorem proof (2013)
  16. Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent: A machine-checked proof of the odd order theorem (2013)
  17. Gonthier, Georges; Ziliani, Beta; Nanevski, Aleksandar; Dreyer, Derek: How to make ad hoc proof automation less ad hoc (2013)
  18. Heras, Jónathan; Komendantskaya, Ekaterina: ML4PG in computer algebra verification (2013)
  19. Rubio, Julio: On the role of formalization in computational mathematics (2013)
  20. Affeldt, Reynald; Hagiwara, Manabu: Formalization of Shannon’s theorems in SSReflect-Coq (2012)

1 2 3 next