Dependent Types Courses and Certifications

Introduction to programming with dependent types in Scala

Explore type theory, dependent types, and theorem proving in Scala. Learn advanced concepts like type families, inductive types, and type-level programming for robust software development.

• Stepik
• On-Demand
• Free Online Course

Strange Loop Conference

Proof Theory Impressionism - Blurring the Curry-Howard Line

Exploring approaches to bridge the gap between proof assistants and production languages, focusing on Rust and its potential for incorporating provable system capabilities.

• YouTube
• 35 minutes
• On-Demand
• Conference Talk

Hausdorff Center for Mathematics

Peter Dybjer - Intuitionistic Type Theory - Lecture I

Explore intuitionistic type theory's foundations, historical context, and applications in mathematics and computer science with Prof. Peter Dybjer's comprehensive lecture.

• YouTube
• 1 hour 1 minute
• On-Demand
• Free Online Course

Strange Loop Conference

Scala vs Idris - Dependent Types, Now and in the Future

Exploring dependent types in Scala and Idris: current capabilities, limitations, and future possibilities. Demonstrates rich type systems' potential for program verification and static constraint capture in functional programming.

• YouTube
• 40 minutes
• On-Demand
• Conference Talk

GOTO Conferences

A Taste of Type Theory

Explore the foundations of type theory in programming, from algebraic data types to dependent types, with insights on mathematical connections and future developments in the field.

• YouTube
• 54 minutes
• On-Demand
• Conference Talk

Institute for Advanced Study

On Voevodsky's Univalence Principle - André Joyal

Explorez le principe d'univalence de Voevodsky avec André Joyal, examinant ses implications pour la théorie des types et les catégories dans cette conférence commémorative approfondie.

• YouTube
• 1 hour 23 minutes
• On-Demand
• Free Online Course

Institute for Advanced Study

Univalent Foundations and the Equivalence Principle - Benedikt Ahrens

Explore univalent foundations and the equivalence principle in mathematics, covering type theory, dependent types, and their applications to structures like monoids and categories.

• YouTube
• 1 hour 1 minute
• On-Demand
• Free Online Course

Strange Loop Conference

Dependent Types in Haskell

Explore dependent types in Haskell, their influence on GHC, and practical applications through an extended example. Learn about current capabilities, challenges, and surprises in language design.

• YouTube
• 39 minutes
• On-Demand
• Conference Talk

Strange Loop Conference

A Little Taste of Dependent Types

Explore dependent types, uniting programming and mathematical proofs. Learn about Pie, a tiny dependently typed language, and see a proof that's also a program.

• YouTube
• 39 minutes
• On-Demand
• Conference Talk

EuroPython Conference

Bulletproof Python - Writing Fewer Tests with a Typed Code Base

Explore how a fully typed Python codebase can reduce the need for extensive testing, leveraging dependent types and exhaustiveness checking to enhance code reliability and efficiency.

• YouTube
• 26 minutes
• On-Demand
• Conference Talk

Hausdorff Center for Mathematics

HOL with Dependent Types and Subtyping

Explore advanced type theory concepts combining Higher-Order Logic, dependent types, and subtyping for enhanced formal reasoning and theorem proving capabilities.

• YouTube
• 33 minutes
• On-Demand
• Free Online Course