graded-haskell
Dependent type systems
Mechanizations for two dependently-typed languages with graded types
Graded Dependent Type systems
23 stars
5 watching
1 forks
Language: Coq
last commit: over 1 year ago coqmetalib
Related projects:
| Repository | Description | Stars |
|---|---|---|
| sweirich/dth | Exploring and showcasing examples of dependently-typed programs in Haskell | 302 |
| sweirich/challenge | An implementation of a strongly-typed System F in Haskell | 117 |
 andreasabel/miniagda | A research prototype of a dependently typed language with sized types and variances | 104 |
 i-am-tom/learn-me-a-haskell | Learning Haskell with focus on dependent types and type-level programming using the OneOf data structure | 70 |
 ilya-klyuchnikov/lambdapi | Reorganization of source code for dependently typed lambda calculus paper to improve readability and understandability | 112 |
 def-/ghc-vis | Visualizes live Haskell data structures in an interactive development environment. | 135 |
 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 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 pikelet-lang/pikelet | A systems programming language with first-class types, designed to support dependent records and types. | 610 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 haskell-gi/haskell-gi | Generates Haskell bindings for GObject Introspection capable libraries | 290 |
 arthuraa/deriving | Automatically generates boilerplate code for Coq inductive types | 24 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 167 |
 ditto/ditto | An experimentally designed dependently typed programming language with a focus on type checking and research | 173 |
 clash-lang/clash-compiler | A compiler that transforms high-level Haskell descriptions into synthesizable hardware descriptions. | 1,442 |