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 48 articles )

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

1 2 3 next

  1. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  2. Lambán, Laureano; Martín-Mateos, Francisco J.; Rubio, Julio; Ruiz-Reina, José-Luis: Using abstract stobjs in ACL2 to compute matrix normal forms (2017)
  3. Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)
  4. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  5. Doczkal, Christian; Smolka, Gert: Completeness and decidability results for CTL in constructive type theory (2016)
  6. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  7. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  8. Sinchuk, Sergey; Chuprikov, Pavel; Solomatov, Konstantin: Verified operational transformation for trees (2016)
  9. Asperti, Andrea: Computational complexity via finite types (2015)
  10. Asperti, Andrea; Ricciotti, Wilmer: A formalization of multi-tape Turing machines (2015)
  11. Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent: Formally verified certificate checkers for hardest-to-round computation (2015)
  12. Affeldt, Reynald; Hagiwara, Manabu; Sénizergues, Jonas: Formalization of Shannon’s theorems (2014)
  13. Aransay, Jesús; Divasón, Jose: Formalization and execution of linear algebra: from theorems to algorithms (2014)
  14. Bartzia, Evmorfia-Iro; Strub, Pierre-Yves: A formal library for elliptic curves in the Coq proof assistant (2014)
  15. Cohen, Cyril; Mörtberg, Anders: A Coq formalization of finitely presented modules (2014)
  16. Heras, Jónathan; Komendantskaya, Ekaterina: Recycling proof patterns in Coq: case studies (2014)
  17. Poza, María; Domínguez, César; Heras, Jónathan; Rubio, Julio: A certified reduction strategy for homological image processing (2014)
  18. Zsidó, Julianna: Theorem of three circles in Coq (2014)
  19. Doczkal, Christian; Kaiser, Jan-Oliver; Smolka, Gert: A constructive theory of regular languages in Coq (2013)
  20. Gonthier, Georges: Engineering mathematics: the odd order theorem proof (2013)

1 2 3 next