A Taste of Type Theory
Offered By: GOTO Conferences via YouTube
Course Description
Overview
Explore the foundations of type theory in programming through this 54-minute conference talk from YOW! 2019. Delve into the deep-rooted connections between types in programming and mathematics, covering topics such as algebraic data types, inductive types, and dependent types. Learn about equalities, natural numbers, and the Curry-Howard correspondence. Discover identity types and their elimination, and gain insights into homotopy type theory. Conclude with a discussion on Zeno's Paradox and its relation to type theory. Enhance your understanding of the theoretical underpinnings of programming languages and their mathematical foundations.
Syllabus
Introduction
Outline
Equalities
Natural Numbers
Dependent Types
Induction on Nats
Curry Howard
Identity Type
refl
Elimination
Zeno's Paradox
Taught by
GOTO Conferences
Related Courses
Addressing Algorithmic BiasGOTO Conferences via YouTube Empowering Consumers - Evolution of Software in the Future
GOTO Conferences via YouTube Why Static Typing Came Back
GOTO Conferences via YouTube Higher Kinded Types in a Lower Kinded Language - Functional Programming in Kotlin
GOTO Conferences via YouTube It's Not Hard to Test Smart - Delivering Customer Value Faster
GOTO Conferences via YouTube