metalib
Metatheory Library
A Coq-based metatheory library providing tools and examples for mechanizing programming language definitions and reasoning about them.
The Penn Locally Nameless Metatheory Library
71 stars
17 watching
23 forks
Language: Coq
last commit: 5 months ago
Linked from 1 awesome list
Related projects:
| Repository | Description | Stars |
|---|---|---|
| plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
 mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 41 |
 coq-community/dblib | A Coq library for manipulating binding structures in syntax with binders. | 30 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
| plclub/hs-to-coq | A tool that translates Haskell code to equivalent Coq code | 78 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 socathie/circomlib-ml | Provides pre-built, modular, and reusable components for machine learning and cryptographic computations | 166 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 kuanweeloong/baremetallib | An experimental C++ header-only support library for bare-metal programming with constraints to simplify the development of embedded systems code. | 2 |
| mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 147 |
 inqwire/quantumlib | A Coq library for reasoning about quantum programs | 32 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
 tacticalmelonfarmer/cxl | A C++17 metaprogramming library providing utilities for strings, parsing, typelists, aggregates to tuples conversions and constant integral literals. | 50 |
 ml4tp/gamepad | A platform that exposes Coq proofs to machine learning algorithms | 72 |