abstract:
The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In this talk, I’ll describe several limitations of modern dependently-typed languages that are holding them back from wider adoption for practical programming. I’ll explain the historical and mathematical reasons for these limitations, and describe how we attempted to relax them in the design of the Zombie research language.
bio:
Chris Casinghino is a Senior Member of the Technical Staff at Draper Laboratory, where he develops static analysis tools in Haskell. In 2014, he completed a PhD in the programming languages group at The University of Pennsylvania. His doctoral research focused on dependently typed programming languages, exploring both their semantics and how to use them to write better programs.