This repository collects some links and resources for learning about type theory, functional programming, and related subjects.
- 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.
- 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.
- 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.
- 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, Martin Escardo, 2004.
- Topological domain theory, Alex Simpson, et al.
- 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, from Saarland U. (downloadable)
- 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 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 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
- 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.
-
- Verified functional programming in Agda (book), Aaron Stump.
- Dependent Types at Work, introductory tutorial by Ana Bove and Peter Dybjer.
- Seemingly impossible constructive proofs, Martin Escardo, 2014.
- Dependently typed metaprogramming (course), Connor McBride, 2013.
- Computer aided formal reasoning (course), Thorsten Altenkirch, 2010.
- Learn you an agda, a modified version of Liam O'Connor's introductory tutorial.
- The Agda Wiki
-
- 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.
-
- 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 Martin Escardo.
-
- 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.
-
- Official homepage
- Official github
- Community homepage
- Community github
- Lean Live! or, "Blean" (weB lean)
- 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
-
- 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.
- agda/agda
- atom/atom
- coq/coq
- idris-lang/Idris-dev
- scala/scala
- HoTT/book for the HoTT book (clone it to get the latest edition)
- edwinb/TypeDD-Samples to accompany the book "TDD in Idris"
- fpinscala/fpinscala to accompany the book "FP in Scala"
- spark-in-action/first-edition to accompany the book "Spark in Action"
- databricks/learning-spark to accompany the book "Learning Spark"
- java8/Java8InAction to accompany the book "Java 8 in Action"
- homotopytypetheory.org
- Francois Dorais' blog posts about doing math in HoTT.
- types-forum and types-announce mailing lists.
- types project