Podcasts Technology Iowa Type Theory Commute Types should be erased for executing and reasoning about programs

Types should be erased for executing and reasoning about programs

Published: Jan. 29, 2020, 8 p.m.

b'

In which I argue that type information should be erased from programs by the compiler both for final execution and also for reasoning (in a language with dependent types, for example, where we can reason about program execution statically).

'