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

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

1 2 3 4 next

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

1 2 3 4 next