In this episode I talk to Elisabeth Stenholm about dependent types, proof assistans and homotopy type theory! If you're ready to take your type safety to the next level, then this episode is for you!

We cover topics like:

Homotopy type theory

Proof assistants

Languages Rocq, Lean4, Agda, Idris

Proving theorems in Lean4

How to get started with dependent types and proof assistants

Links

• Theorems for free 
• Propositions as types
• Elisabeth’s Func Prog presentation 
• Formally verified C compiler 
• Property-based testing in F#
• Building Idris in Idris 
• Elisabeth's PhD thesis