Tech talk: Designing a practical dependently typed language

  • Date Wednesday, November 11, 2015  Time 11:00 AM
  • Speaker Chris Casinghino
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

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.

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.