marshall-lee / software_foundations
My solutions to Software Foundations course in Coq proof assistant.
☆33Updated 7 months ago
Alternatives and similar repositories for software_foundations:
Users that are interested in software_foundations are comparing it to the libraries listed below
- PL conference deadline countdowns☆55Updated last week
- ☆40Updated 2 months ago
- Lean 4 port of Iris, a higher-order concurrent separation logic framework☆80Updated this week
- Coq code formatter☆22Updated this week
- A monadic library for symbolic evaluation☆58Updated last week
- ☆24Updated 5 years ago
- Experiments in automation for Lean☆92Updated last week
- Visual Studio Code Extension and Language Server Protocol for Coq☆159Updated this week
- Separation Logic Proofs in Lean☆34Updated 2 months 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
- Lean4 Logic Formalization☆97Updated this week
- Formalizing Euclidean Geometry in Lean☆29Updated 11 months ago
- A mechanisation of Wasm in Coq(Rocq)☆101Updated 3 weeks ago
- Communication between Coq and SAT/SMT solvers☆158Updated 5 months ago
- Visual Studio Code extension for Coq☆362Updated this week
- Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]☆117Updated last week
- A verified polyhedral scheduling validator in Coq.☆19Updated 4 months ago
- A formalization of the textbook Elements of Set Theory☆59Updated 3 years ago
- Theorem Proving in Lean 4☆173Updated 4 months ago
- [FSE-2024] Towards AI-Assisted Synthesis of Verified Dafny Methods☆40Updated 8 months ago
- A (WIP) equality saturation tactic for Lean based on egg.☆55Updated this week
- Ltac2 tutorial☆43Updated 2 years ago
- CS 704 course website - Principles of Programming Languages☆67Updated 2 years ago
- Type Checking in Lean 4☆26Updated 5 months ago
- The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)☆51Updated 10 months ago
- We combat sloppy arguments in competitive programming and raise the standard of rigor☆22Updated 2 months ago
- Natural language tactics to teach mathematics using Lean 4☆60Updated this week
- An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logt…☆139Updated 4 months ago
- A Seamless, Interactive Tactic Learner and Prover for Coq☆60Updated 3 weeks ago
- Exercises and other materials for the course on FP and QuickCheck at Peking University in October 2023☆34Updated last year