dot-calculus
Type System Compiler
A formalization of Dependent Object Types (DOT) calculus in Coq to support type safety proofs for a new foundation for Scala's type system
Formalization of the Dependent Object Types (DOT) calculus
62 stars
5 watching
9 forks
Language: Coq
last commit: over 2 years ago
Linked from 1 awesome list
xgrommx/awesome-functional-programmingRelated projects:
| Repository | Description | Stars |
|---|---|---|
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 155 |
 blaisorblade/dot-iris | Mechanized formalization of soundness for DOT with logical relations in Coq | 30 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 mattam82/coq-equations | A package for defining functions in Coq using dependent types and pattern-matching. | 223 |
 pedrotst/coquedille | Translates Coq terms into Cedille terms for a specific domain-specific language | 33 |
 coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 sweirich/graded-haskell | Mechanizations for two dependently-typed languages with graded types | 24 |
 0xd34df00d/refinedt | A project that formalizes refinement types and dependent types in the Agda language | 58 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 affeldt-aist/infotheo | A formalization of information theory and linear error-correcting codes in Coq. | 64 |
| coq-community/math-classes | A library of abstract interfaces for various mathematical structures to facilitate algebraic manipulation and type class-based reasoning in Coq | 162 |