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

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

1 2 3 4 next

  1. Wang, Qingxiang; Kaliszyk, Cezary: JEFL: joint embedding of formal proof libraries (2021)
  2. Doczkal, Christian; Pous, Damien: Graph theory in Coq: minors, treewidth, and isomorphisms (2020)
  3. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  4. Ramos, Marcus V. M.; Bacelar Almeida, José Carlos; Moreira, Nelma; de Queiroz, Ruy J. G. B.: Some applications of the formalization of the pumping lemma for context-free languages (2019)
  5. Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien: Formalization techniques for asymptotic reasoning in classical analysis (2018)
  6. Benzaken, V.; Contejean, É.; Keller, Ch.; Martins, E.: A Coq formalisation of SQL’s execution engines (2018)
  7. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  8. Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric: Foundations of dependent interoperability (2018)
  9. Doczkal, Christian; Combette, Guillaume; Pous, Damien: A formal proof of the minor-exclusion property for treewidth-two graphs (2018)
  10. Doczkal, Christian; Smolka, Gert: Regular language representations in the constructive type theory of Coq (2018)
  11. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  12. Parsert, Julian; Kaliszyk, Cezary: Towards formal foundations for game theory (2018)
  13. Sakaguchi, Kazuhiko: Program extraction for mutable arrays (2018)
  14. Bagnall, Alexander; Merten, Samuel; Stewart, Gordon: A library for algorithmic game theory in \textsfSsreflect/Coq (2017)
  15. Benzaken, Véronique; Contejean, Évelyne; Dumbrava, Stefania: Certifying standard and stratified Datalog inference engines in SSReflect (2017)
  16. Chen, Ran; Lévy, Jean-Jacques: A semi-automatic proof of strong connectivity (2017)
  17. Komendantskaya, Ekaterina; Heras, Jónathan: Proof mining with dependent types (2017)
  18. 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)
  19. Ahrens, Benedikt; Mörtberg, Anders: Some wellfounded trees in UniMath (extended abstract) (2016)
  20. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in \textscCoq (2016)

1 2 3 4 next