TypeFunc

This repository collects some links and resources for learning about type theory, functional programming, and related subjects.

My Current Favorites (new section!)

Because there are so many (perhaps too many) links to resources on this page, I've decided to occasionally short-list a few resources that were (at the time of the last commit) my current favorites... for whatever that's worth.

1. Introduction to Univalent Foundations of Mathematics with Agda, Martín Escardó, 2019.
2. The Agda Universal Algebra Library, William DeMeo, 2021. (shameless plug).
3. Homotopy Type Theory Electronic Seminar Talks.
4. The HoTT Book, textbook from the IAS year on univalent foundations, 2013.
5. Scala with Cats, Noel Welsh and Dave Gurnell, 2020.

What appeals to me about the last item is the book's promotion of program composition and category theory as two powerful organizing principles for software design and development.

Books and Papers

Basics/Background

• Logic and Proof (source), Avigad, Lewis, van Doorn.
• Type Theory and Formal Proof: An Introduction, Geuvers and Nederpelt.
• Foundations for Programming Languages, John Mitchell.
• Types and Programming Languages, Benjamin Pierce.
• Practical Foundations for Programming Languages, Robert Harper.
• Proofs and Types, Girard, Lafont, Taylor.
• Computational Category Theory, Rydeheard and Burstall.
• Categories for Types, Roy Crole.
• Category Theory in Context, Emily Riehl.
• Type Theory and Functional Programming, Simon Thompson.
• Intuitionistic Type Theory, Per Martin-Löf's Padova lectures.
• Two Lectures on Contructive Type Theory, Robert Constable.

Programming Books

• Type-Driven Development with Idris, Edwin Brady.
• Functional Programming in Scala, Paul Chiusano and Rúnar Bjarnason.
• Software Foundations, Pierce, et al.
• Verified Functional Programming in Agda, Aaron Stump.

More Advanced

• Domain-theoretic Foundations of Functional Programming
• Advanced Topics in Types and Programming Languages, Pierce ed., 2005.
• Higher-Order Computability, Longley, Normann, 2015.
• The HoTT Book, many authors, a textbook on informal type theory, 2013.
• Introduction to Homotopy Type Theory, Thorsten Altenkirch's lecture notes, 2017.
• Programming in Martin-Löf's Type Theory, Nordström, Petersson, Smith, 1990.
• Lectures on the Curry-Howard Isomorphism, Sørensen, Urzyczyn, 1998.
• Synthetic Topology of data types and classical spaces, Martín Escardó, 2004.
• Topological domain theory, Alex Simpson, et al.

---

Recorded Lectures

• Foundations of Math: Univalent Foundations & Set Theory, ​​​Bielefeld, DE, 2016.
• IHP Semantics of proofs and certified math, Institute Henri Poincare, FR, 2014.
• Homotopy Type Theory graduate seminar, Robert Harper, CMU, 2013.
• Idris course at ITU, by Edwin Brady, Copenhagen, DK, 2013.
• IAS Univalent Foundations Program, 2012--2013.
• The Five Stages of Accepting Constructive Math, Andrej Bauer, IAS, 2013.
• Introductory Coq tutorials, Andrej Bauer.
• Introduction to computational logic, Chad Brown (downloadable)

---

Courses

• 2021 Agda Tutorial in Advanced Functional Programming, Andreas Abel.
• 2019 Introduction to Univalent Foundations of Mathematics with Agda, Martín Escardó.
• 2019 Homotopy (type) theory, Andrej Bauer and Jaka Smrekar.
• 2017 Type Theory, Andreas Abel.
• 2017 Mathematical Foundations of Programming, Venanzio Capretta.
• 2017 Coalgebras and Infinite Data Structures, Venanzio Capretta.
• 2017 Naïve Type Theory (YouTube videos), Thorsten Altenkirch.
• 2015 Denotational Semantics, Marcelo Fiore.
• 2015 Introduction to Computational Logic, Gert Smolka and Tobias Tebbi.
• 2014 Semantics of proofs and certified mathematics, Institute Henri Poincare.
• 2014 Coalgebra, Sam Staton and Alexandra Silva.
• 2014 Software Foundations, Stephanie Weirich.
• 2014 Programs and Proofs: mechanizing math with dependent types, Ilya Sergey.
• 2013 Homotopy Type Theory graduate seminar, Robert Harper.
• 2013 Dependently typed metaprogramming, Connor McBride.
• 2013 Functional programming principles in Scala, Martin Odersky.
• 2012 short course on category theory, Steve Awodey (textbook).
• 2012 short course on topology for functional programming, Martin Escardo.
• 2011 Introduction to Formal Reasoning Thorsten Altenkirch.
• 2011 course on type theory and Coq, Radboud University, NL.
• 2011 course on verifying algorithms in Coq, CEA-EDF-INRIA, FR.
• 2010 Categorical Logic, Samuel Staton.
• Oregon Programming Languages Summer School
  • 2019: probabilistic programming and security
  • 2018: parallelism and concurrency
  • 2017: a spectrum of types.
  • 2016: types, logic, semantics, and verification.
  • 2015: types, logic, semantics, and verification.
  • 2014: types, logic, semantics, and verification.
  • 2013: types, logic, and verification.
  • 2012: logic, languages, compilation, and verification. (Lectures@YouTube)
• Midlands Graduate School on foundations of computer science
  • 2019: Birmingham
  • 2018: Nottingham
  • 2017: Leicester
  • 2016: Birmingham
  • 2015: Sheffield
  • 2014: Nottingham
• CMU courses
  • 2013 grad seminar on HoTT, Robert Harper, with recorded lectures.
  • 2012 grad course on linear logic, Frank Pfenning.
  • 2010 grad course on modal logic, Frank Pfenning and André Platzer.
  • 2009 undergrad course on constructive logic, Frank Pfenning and Ron Garcia.

---

Programming Languages (in alphabetical order)

• Agda

  • General Resources
    • The Agda Wiki
    • Dependent Types at Work, introductory tutorial by Ana Bove and Peter Dybjer.
    • Computer aided formal reasoning (course), Thorsten Altenkirch, 2010.
    • Agda Tutorial in Advanced Functional Programming, Andreas Abel, 2021.
  • Resources with a Mathematics focus
    • Introduction to Univalent Foundations with Agda, Martín Escardó, 2019.
    • The Agda Universal Algebra Library, William DeMeo, 2021.
    • YouTube: Cubical Agda and its extensions, Andrea Vezzosi, 2021.
    • Seemingly impossible constructive proofs, Martín Escardó, 2014.
  • Resources with a Programming Languages focus
    • Programming Language Foundations in Agda, Philip Wadler.
    • Verified functional programming in Agda (book), Aaron Stump.
    • Dependently typed metaprogramming (course), Conor McBride, 2013.

• Coq

  • Software Foundations (book), Pierce, et al.
  • Certified Programming with Dependent Types (book), Adam Chlipala.
  • YouTube: introductory Coq tutorials, by Andrej Bauer.
  • Gentle Intro to Type Classes in Coq, Casteran and Sozeau.
  • Type Classes for Math in Type Theory (paper) (repository), Spitters and van der Weegen.
  • General Algebra in Coq (thesis), Venanzio Capretta.
  • UniMath Coq Library for univalent foundations, Voevodsky, et al.
  • Type theory and Coq (course) Radboud University, NL.
  • Software Foundations in Coq, tips from OPLSS.

• Haskell

  • Learn You a Haskell for Great Good! (book), a beginner's guide that's free to read online.
  • Stephen Diehl has some nice posts covering things like monads in Haskell.
  • School of Haskell at fpcomplete.com, a commercial site that seems to allow free creation and sharing of online projects; offers many resources for learning Haskell.
  • A monad for infinite search in finite time, by Martín Escardó.

• Idris

  • The Idris Tutorial.
  • Type-Driven Development with Idris (book), Edwin Brady.
  • Kats Idris Workshop, Dublin, IR, 2016.
  • Idris Course at ITU, Edwin Brady, Copenhagen, DK, 2013.

• Lean

  • Official homepage
  • Official github
  • Community homepage
  • Community github
  • Lean Live! or, "Blean" (weB lean)
    • official
    • lean-community
  • Documentation
    • Intro to Lean
    • Theorem Proving in Lean
    • Programming in Lean
    • Logic and Proof (source), CMU Undergrad Course.
    • ualib.org documentation for the Lean Universal Algebra Library.
  • Lean zulip chatroom
  • Lean zulip archive

• Scala

  • Functional Programming in Scala (book), Paul Chiusano and Rúnar Bjarnason, 2014.
  • Functional Programming Principles in Scala (course), Martin Odersky.
  • Principles of Reactive Programming (course), Odersky, Meijer, Kuhn.
  • Ninety-Nine Scala Problems, Gold and Hett.

---

Some Related GitHub Repositories

(alphabetical)

• agda/agda
• atom/atom
• coq/coq
• databricks/learning-spark to accompany the book "Learning Spark"
• edwinb/TypeDD-Samples to accompany the book "TDD in Idris"
• fpinscala/fpinscala to accompany the book "FP in Scala"
• HoTT/book for the HoTT book (clone it to get the latest edition)
• idris-lang/Idris-dev
• java8/Java8InAction to accompany the book "Java 8 in Action"
• scala/scala
• spark-in-action/first-edition to accompany the book "Spark in Action"
• ualib/ualib.gitlab.io source code for The Agda Universal Algebra Library

Miscellaneous

• homotopytypetheory.org
• Francois Dorais' blog posts about doing math in HoTT.
• types-forum and types-announce mailing lists.
• types project