Episode 4: Stephanie Weirich on Zombie and Dependent Haskell

In our fourth episode, we speak with Stephanie Weirich from the University of Pennsylvania on the Zombie language and Dependent Haskell. Stephanie is a long-time contributor to Haskell, having been involved in the design and implementation of features such as generalized algebraic datatypes, higher-rank polymorphism, type families, and promoted datatypes. She has also been a participant in Trellys, a project with the goal of combining proofs and programming in the same language. Zombie is a different kind of dependently typed language, eschewing automatic β-reduction in the type checker for an approach based on explicit equality rewriting, which enables new ways of combining proofs and programs, as well as new forms of proof automation. Meanwhile, as languages designed for dependently typed programming come closer to practical applicability, Haskell is also moving towards full dependent types. We discuss the challenges and opportunities available at the cutting edge of Haskell.

You can listen to Episode 4: Stephanie Weirich on Zombie and Dependent Haskell online on Radio and Podcast. Open the player on this page to stream the available audio.

Episode 4: Stephanie Weirich on Zombie and Dependent Haskell is an episode from The Type Theory Podcast by David Raymond Christiansen.

This episode is 00:00:00 long.

This episode was published on Apr 18, 2015.

Yes. Use the heart button on the episode page to add it to your favorite episodes list.

Yes. This page shows related episodes from The Type Theory Podcast when more episodes are available from the podcast feed.