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

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

1 2 3 next

  1. Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien: Formalization techniques for asymptotic reasoning in classical analysis (2018)
  2. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
  3. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  4. Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
  5. Doczkal, Christian; Combette, Guillaume; Pous, Damien: A formal proof of the minor-exclusion property for treewidth-two graphs (2018)
  6. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  7. Parsert, Julian; Kaliszyk, Cezary: Towards formal foundations for game theory (2018)
  8. Sakaguchi, Kazuhiko: Program extraction for mutable arrays (2018)
  9. Bagnall, Alexander; Merten, Samuel; Stewart, Gordon: A library for algorithmic game theory in \textsfSsreflect/Coq (2017)
  10. Benzaken, Véronique; Contejean, Évelyne; Dumbrava, Stefania: Certifying standard and stratified Datalog inference engines in SSReflect (2017)
  11. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  12. 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)
  13. Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)
  14. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in \textscCoq (2016)
  15. Doczkal, Christian; Smolka, Gert: Completeness and decidability results for CTL in constructive type theory (2016)
  16. Grimm, José: Implementation of Bourbaki’s elements of mathematics in Coq: part two, from natural numbers to Real numbers (2016)
  17. Kuga, Ken’ichi; Hagiwara, Manabu; Yamamoto, Mitsuharu: Formalization of Bing’s shrinking method in geometric topology (2016)
  18. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  19. Sinchuk, Sergey; Chuprikov, Pavel; Solomatov, Konstantin: Verified operational transformation for trees (2016)
  20. Asperti, Andrea: Computational complexity via finite types (2015)

1 2 3 next