Here's some exciting work on type preserving compilation for dependent types, years in the making! We still have a long way to go, but this kind of work makes me excited and hopeful for the future.
Quote Tweet
My dissertation has been accepted by the admin and publishing people, so here it is:
williamjbowman.com/#dissertation
Show this thread