W-in-Coq
Type inference tool verifier
A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools.
This is a Coq formalization of Damas-Milner type system and its algorithm W.
25 stars
3 watching
1 forks
Language: Coq
last commit: over 4 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 220 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 arthuraa/deriving | Automatically generates boilerplate code for Coq inductive types | 24 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 82 |
 samuelgruetter/dot-calculus | A formalization of Dependent Object Types (DOT) calculus in Coq to support type safety proofs for a new foundation for Scala's type system | 62 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 437 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |