-
vector-bingo: Simple introduction (PLMW 2018)
- Using length-indexed lists to implement a bingo game
-
regexp: Example code from "Dependent Types in Haskell"
- Dependently-Typed Regular Expression Submatching
-
depending-on-types: Example code from "Depending on Types"
- Red/Black trees that statically preserve their invariants
-
examples: Other examples of dependently-typed GHC
-
talks: Slides from presentations
- "Dependending on Types", ICFP 2014, CodeMesh 2015, Typelevel Summit 2016
- "The Influence of Dependent Types", POPL 2017
- "Dependently-Typed Haskell", StrangeLoop 2017
- "Dependent Types in Haskell", McMaster 2017, UW 2017, and Comcast FP 2018
forked from sweirich/dth
-
Notifications
You must be signed in to change notification settings - Fork 0
stjordanis/dth
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
About
Examples of Dependently-typed programs in Haskell
Resources
Code of conduct
Security policy
Stars
Watchers
Forks
Packages 0
No packages published
Languages
- Haskell 93.6%
- Agda 6.4%