cz717 / bksol
☆10Updated 8 years ago
Alternatives and similar repositories for bksol:
Users that are interested in bksol are comparing it to the libraries listed below
- Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]☆117Updated this week
- Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintaine…☆71Updated last month
- CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory☆225Updated 2 months ago
- Collection of errata for book Aarne Ranta, Implementing Programming Languages☆12Updated 2 years ago
- A formalization of the textbook Elements of Set Theory☆59Updated 3 years ago
- PL conference deadline countdowns☆55Updated last week
- A function definition package for Coq☆226Updated 2 weeks ago
- Metaprogramming, verified meta-theory and implementation of Coq in Coq☆420Updated this week
- A Verified Compiler for Gallina, Written in Gallina☆140Updated 3 weeks ago
- ☆227Updated 6 months ago
- A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]☆165Updated 3 months ago
- Notes on higher-order typed compilation. Probably wrong☆23Updated 2 years ago
- Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]☆113Updated 3 weeks ago
- Organization and planning for the Initial Types Club☆72Updated 2 years ago
- Tricks you wish the Coq manual told you [maintainer=@tchajed]☆513Updated last week
- Randomized Property-Based Testing Plugin for Coq☆263Updated 2 weeks ago
- Archive for all Coq related OPAM packages organized in various repositories☆133Updated this week
- EPIT 2020 - Spring School on Homotopy Type Theory☆103Updated 3 years ago
- A monadic library for symbolic evaluation☆58Updated last week
- Communication between Coq and SAT/SMT solvers☆158Updated 5 months ago
- Visual Studio Code extension for Coq☆362Updated this week
- Logical manifestations of topological concepts, and other things, via the univalent point of view.☆243Updated this week
- ☆19Updated 7 years ago
- Proof assistant based on the λΠ-calculus modulo rewriting☆304Updated this week
- Exercises from https://softwarefoundations.cis.upenn.edu/lf-current/index.html☆9Updated 6 years ago
- Appendix of "Principles of Abstract Interpretation", P. Cousot, MIT Press, 2021, containing the proofs and the solutions of exercises not…☆41Updated 3 years ago
- ☆236Updated last week
- A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]☆338Updated last month
- Multi platform setup for Coq, Coq libraries and tools☆192Updated 2 weeks ago
- A work-in-progress language and compiler for verified low-level programming☆302Updated last week