dot
Type theory proof
Mechanized proof of soundness for a type-theoretic foundation for languages like Scala
formalization of the Dependent Object Types (DOT) calculus
154 stars
17 watching
12 forks
last commit: about 8 years ago
Linked from 1 awesome list
coqdafnymeta-theoryoopplt-redextwelf
xgrommx/awesome-functional-programmingRelated projects:
| Repository | Description | Stars |
|---|---|---|
 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 |
 blaisorblade/dot-iris | Mechanized formalization of soundness for DOT with logical relations in Coq | 30 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 93 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 jetbrains/arend | A theorem prover and a programming language based on Homotopy Type Theory | 694 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 jozefg/learn-tt | A collection of resources for learning type theory and related fields | 2,161 |
 eashanhatti/konna | An experimental language exploring two-level type theory to achieve compile-time evaluation of dynamic features | 11 |
 maxwell-thum/typst-pf3 | A LaTeX style port from Leslie Lamport's pf2.sty to Typst for writing structured proofs. | 3 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 williamdemeo/typefunc | Collects links and resources on type theory and functional programming. | 309 |
 mplatvoet/funktional | A Kotlin implementation of monadic types for functional programming. | 10 |
 mknejp/dotvariant | A type-safe sum type library for C# that enables the creation of compact variants with compile-time checked constraints and generated interfaces. | 70 |
 0xd34df00d/refinedt | A project that formalizes refinement types and dependent types in the Agda language | 58 |