An expressive, scalable type theory for certified code.

Karl Crary, Joseph Vanderwaart

Browse the full ICFP paper archive.