refinedt
Type system formalism
A project that formalizes refinement types and dependent types in the Agda language
Refinement types + dependent types = ❤️
58 stars
8 watching
6 forks
Language: Agda
last commit: over 3 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 fthomas/refined | A Scala library that allows adding constraints to types at compile-time using type-level predicates. | 1,715 |
 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 |
 mrkkrp/facts | A Haskell library for working with refined types to represent and manipulate data structures | 57 |
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 155 |
 andreasabel/miniagda | A research prototype of a dependently typed language with sized types and variances | 104 |
 informalsystems/quint | A specification language with type checking and tooling based on temporal logic of actions | 834 |
 ditto/ditto | An experimentally designed dependently typed programming language with a focus on type checking and research | 173 |
 sweirich/graded-haskell | Mechanizations for two dependently-typed languages with graded types | 24 |
 superstar64/aith | A language project that aims to create a systems programming language with a strong emphasis on type systems and advanced features like levity polymorphism, first-class inline functions, linear types, and effectful regions. | 64 |
 andrew-johnson-4/lsts | A programming language and proof assistant built on top of Rust. | 114 |
 jfecher/ante | A systems language focused on refinement types and lifetime inference | 1,920 |
 typedefs/typedefs | A language-agnostic way to define algebraic data types using polynomials. | 367 |
 jetbrains/arend | A theorem prover and a programming language based on Homotopy Type Theory | 698 |
 jozefg/learn-tt | A collection of resources for learning type theory and related fields | 2,180 |
 s-expressionists/ctype | An implementation of the Common Lisp type system focusing on precise and simplified reification of type specifiers | 26 |