Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

A Little Taste of Dependent Types

Strange Loop Conference via YouTube

Overview

Save Big on Coursera Plus. 7,000+ courses at $160 off. Limited Time Only!
Explore dependent types in programming and mathematical proofs through a conference talk from Strange Loop. Dive into the world of Pie, a tiny dependently typed language featured in the upcoming book "The Little Typer." Discover how dependent types unite programming and mathematical proofs, allowing the use of familiar programming tools and techniques for mathematical reasoning. Learn about the essential beauty of dependent types, often hidden beneath layers of powerful automatic tools. Follow along as the speaker demonstrates a proof in Pie that doubles as a program, covering topics such as types and programs, addition, doubling, evidence of evenness and oddness, and the relationship between natural numbers and even/odd properties. Gain insights into the potential of dependent types and their gradual progression towards mainstream programming from research languages like Coq, Agda, and Idris.

Syllabus

Intro
Some Momentous Events
Types and Programs
What's a Type?
Addition
Double
There is Evidence
Evidence of Evenness
Is Zero Even?
Evidence of Oddness
All the Evidence
Every Natural Number is Even or Odd
The Step

Taught by

Strange Loop Conference

Reviews

Start your review of A Little Taste of Dependent Types

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.