principia
Notation renderer
A LaTeX package designed to typeset the notation used in Whitehead and Russell's 1910 mathematical treatise
The Principia Rewrite
207 stars
16 watching
5 forks
Language: TeX
last commit: 6 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 | Tools for processing Coq code and prose in technical documents | 236 |
 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 | 384 |
 fluidex/plonkit | Provides tools and utilities for generating and verifying proofs in a zkSNARK proof system | 158 |
 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. | 44 |
 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 | Formalises algebraic combinatorics in Coq using symmetric functions and polynomials | 36 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 93 |