Refinement types + dependent types = ❤️
Agda
62
2,958 commits
updated Aug 8, 2022
The two most important directories are:
toy contains a toy proof-of-concept implementation of a language with refinement types that compiles to Idris.
2,951 commits
3 commits
1 commits
AndrasKovacs/setoidtt
Prototype implementations of systems based on setoid type theory
66
AndrasKovacs/staged
Staged compilation with dependent types
187
AndrasKovacs/implicit-fun-elaboration
Implementation for ICFP 2020 paper
53
alhassy/next-700-module-systems
PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing…
82
jespercockx/agda-lecture-notes
Agda lecture notes for the Functional Programming course at TU Delft
135
HigherOrderCO/Kind
A modern proof language
3,762
AndrasKovacs/sett
Setoid type theory implementation
41
Andromedans/andromeda
A proof assistant for general type theories
317
74.3%
TeX
15.4%
Haskell
10.0%
