principia
Formal notation library
Provides LaTeX macros and tools to typeset logical formalisms inspired by Whitehead and Russell's 1910 work
The Principia Rewrite
208 stars
16 watching
5 forks
Language: TeX
last commit: 11 months ago coqcoq-ecosystemformal-logicformal-mathematicsformal-proofshistory-of-philosophylatexlatex-packageslogic
Related projects:
| Repository | Description | Stars |
|---|---|---|
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 alnkpa/sublimeprolog | Provides syntax highlighting and automated build functionality for a specific logic programming language. | 66 |
 cpitclaudel/alectryon | A tool for processing Coq and Lean 4 code embedded in text documents | 237 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 388 |
 fluidex/plonkit | Provides tools and utilities for generating and verifying proofs in a zkSNARK proof system | 159 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 math-comp/coq-combi | Formalizes algebraic combinatorics and symmetric functions in Coq. | 37 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 94 |