• 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

See also: Strongly-typed System F in a separate repo.