Cover image of The Type Theory Podcast
(5)
Science
Natural Sciences

The Type Theory Podcast

Updated about 1 month ago

Science
Natural Sciences
Read more

A podcast about type theory

Read more

A podcast about type theory

iTunes Ratings

5 Ratings
Average Ratings
5
0
0
0
0

iTunes Ratings

5 Ratings
Average Ratings
5
0
0
0
0
Cover image of The Type Theory Podcast

The Type Theory Podcast

Latest release on Dec 01, 2016

Read more

A podcast about type theory

Rank #1: Episode 6: Aaron Stump on Cedille

Podcast cover
Read more
Episode 6: Aaron Stump on Cedille

Dec 01 2016

Play

Rank #2: Episode 5: Bob Constable on CTT and Nuprl

Podcast cover
Read more
Episode 5: Bob Constable on CTT and Nuprl

Aug 31 2015

Play

Rank #3: Episode 4: Stephanie Weirich on Zombie and Dependent Haskell

Podcast cover
Read more
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.

Apr 18 2015

Play

Rank #4: Episode 3: Dan Licata on Homotopy Type Theory

Podcast cover
Read more
Episode 3: Dan Licata on Homotopy Type Theory

Jan 07 2015

Play

Rank #5: Episode 2: Edwin Brady on Idris

Podcast cover
Read more
In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.

Sep 26 2014

1hr 32mins

Play

Episode 6: Aaron Stump on Cedille

Podcast cover
Read more
Episode 6: Aaron Stump on Cedille

Dec 01 2016

Play

Episode 5: Bob Constable on CTT and Nuprl

Podcast cover
Read more
Episode 5: Bob Constable on CTT and Nuprl

Aug 31 2015

Play

Episode 4: Stephanie Weirich on Zombie and Dependent Haskell

Podcast cover
Read more
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.

Apr 18 2015

Play

Episode 3: Dan Licata on Homotopy Type Theory

Podcast cover
Read more
Episode 3: Dan Licata on Homotopy Type Theory

Jan 07 2015

Play

Episode 2: Edwin Brady on Idris

Podcast cover
Read more
In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.

Sep 26 2014

1hr 32mins

Play

Episode 1: Peter Dybjer on types and testing

Podcast cover
Read more
We speak with Peter Dybjer about the relationship between QuickCheck-style testing and proofs and verification in type theory.

Aug 13 2014

Play

iTunes Ratings

5 Ratings
Average Ratings
5
0
0
0
0