Mathematical Reasoning

Naïve Type Theory by Thorsten Altenkirch

Lecture series on Naïve Type Theory by Thorsten Altenkirch. Introduction to type theory concepts fundamental to proof assistants like Lean and Coq.

Visit Website

About

Lecture series on Naïve Type Theory presented by Thorsten Altenkirch, a leading researcher in type theory and constructive mathematics.

Speaker

Thorsten Altenkirch

  • Professor at University of Nottingham
  • Leading researcher in type theory, constructive mathematics, and functional programming
  • Co-author of the HoTT (Homotopy Type Theory) book
  • Known for work on quotient types, containers, and constructive set theory

Content

Introduction to type theory concepts including:

  • Basic type theory principles
  • Type constructors and eliminators
  • Relationship to logic (Curry-Howard correspondence)
  • Foundations for proof assistants

Relevance

Type theory is the foundation of modern proof assistants like Lean, Coq, and Agda. Understanding type theory is essential for anyone interested in formal verification and AI-assisted theorem proving.

Video

Available on Bilibili with Chinese subtitles/context.

  • HoTT Book: https://homotopytypetheory.org/book/
  • Thorsten Altenkirch’s research page