rhetenor/awesome-awesomeness
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Updating conversion, creating readmes

Browse Source
This commit is contained in:
Jonas Zeunert
2024-04-19 23:37:46 +02:00
parent 3619ac710a
commit 08e75b0f0a
635 changed files with 30878 additions and 37344 deletions
Download Patch File Download Diff File Expand all files Collapse all files

36
terminal/coq
View File

@@ -1,11 +1,10 @@
 Awesome Coq !Awesome (https://awesome.re/badge.svg) (https://awesome.re)
 Awesome Coq !Awesome (https://awesome.re/badge.svg) (https://awesome.re)
 (https://github.com/coq-community/manifesto)
▐ A curated list of awesome Coq libraries, plugins, tools, and resources.
The Coq proof assistant (https://coq.inria.fr) provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of 
machine-checked proofs.
The Coq proof assistant (https://coq.inria.fr) provides a formal language to write mathematical definitions, executable algorithms, and theorems, together with an environment for semi-interactive development of machine-checked proofs.
Contributions welcome! Read the contribution guidelines (https://github.com/coq-community/awesome-coq/blob/master/CONTRIBUTING.md) first.
@@ -28,7 +27,7 @@
 - Course Material (#course-material)
 - Tutorials and Hints (#tutorials-and-hints)
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
Projects
@@ -111,8 +110,8 @@
- AAC Tactics (https://github.com/coq-community/aac-tactics) - Tactics for rewriting universally quantified equations, modulo associativity and commutativity of some operator.
- Coq-Elpi (https://github.com/LPCIC/coq-elpi) - Extension framework based on λProlog providing an extensive API to implement commands and tactics.
- Waterproof proof language (https://github.com/impermeable/coq-waterproof) - Plugin providing a language for writing proof scripts in a style that resembles non-mechanized mathematical proof.
- CoqHammer (https://github.com/lukaszcz/coqhammer) - General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the 
reconstruction of found proofs.
- CoqHammer (https://github.com/lukaszcz/coqhammer) - General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found 
proofs.
- Equations (https://github.com/mattam82/Coq-Equations) - Function definition package for Coq.
- Gappa (https://gitlab.inria.fr/gappa/coq) - Tactic for discharging goals about floating-point arithmetic and round-off errors.
- Hierarchy Builder (https://github.com/math-comp/hierarchy-builder) - Collection of commands for declaring Coq hierarchies based on packed classes.
@@ -123,8 +122,8 @@
- Paramcoq (https://github.com/coq-community/paramcoq) - Plugin to generate parametricity translations of Coq terms.
- QuickChick (https://github.com/QuickChick/QuickChick) - Plugin for randomized property-based testing.
- SMTCoq (https://github.com/smtcoq/smtcoq) - Tool that checks proof witnesses coming from external SAT and SMT solvers.
- Tactician (https://coq-tactician.github.io) - Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to 
automate proof synthesis fully.
- Tactician (https://coq-tactician.github.io) - Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis 
fully.
- Unicoq (https://github.com/unicoq/unicoq) - Plugin that replaces the existing unification algorithm with an enhanced one.
Puzzles and Games
@@ -247,21 +246,18 @@
Books
- Coq'Art (https://www.labri.fr/perso/casteran/CoqArt/) - The first book dedicated to Coq.
- Software Foundations (https://softwarefoundations.cis.upenn.edu) - Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to 
beginners.
- Software Foundations (https://softwarefoundations.cis.upenn.edu) - Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
- Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/) - Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.
- Program Logics for Certified Compilers (https://www.cs.princeton.edu/~appel/papers/plcc.pdf) - Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq 
which is applied to the Clight programming language and other examples.
- Formal Reasoning About Programs (http://adam.chlipala.net/frap/) - Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for 
this purpose.
- Programs and Proofs (https://ilyasergey.net/pnp/) - Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning 
about decidable propositions via a small set of primitives from the SSReflect proof language.
- Program Logics for Certified Compilers (https://www.cs.princeton.edu/~appel/papers/plcc.pdf) - Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the 
Clight programming language and other examples.
- Formal Reasoning About Programs (http://adam.chlipala.net/frap/) - Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
- Programs and Proofs (https://ilyasergey.net/pnp/) - Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable 
propositions via a small set of primitives from the SSReflect proof language.
- Computer Arithmetic and Formal Proofs (http://iste.co.uk/book.php?id=1238) - Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
- The Mathematical Components book (https://math-comp.github.io/mcb/) - Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.
- Modeling and Proving in Computational Type Theory (https://github.com/uds-psl/MPCTT) - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical 
programming.
- Hydras & Co. (https://github.com/coq-community/hydra-battles) - Continuously in-progress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a 
proof of the Gödel-Rosser first incompleteness theorem.
- Modeling and Proving in Computational Type Theory (https://github.com/uds-psl/MPCTT) - Book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.
- Hydras & Co. (https://github.com/coq-community/hydra-battles) - Continuously in-progress book and library on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including a proof of the Gödel-Rosser 
first incompleteness theorem.
Course Material