UH-MFC Bootcamp

During the spring break we will gather for a "bootcamp" which will consist of crash courses on the simply typed lambda calculus and type theory. We will also gain some experience with some software implementations of the theory, like Coq and Agda.

Tentative Schedule

We will meet each day 3/28--4/1 (Tuesday--Sunday) on the fourth floor of Keller Hall at the following times:

Morining Lectures: 11--12:15

Afternoon Sessions: 1:30--3pm

For an indication of which topics will be covered at each meeting, please see the calendar.pdf file in this repository.

Please send quesitons or comments to me: williamdemeo at gmail.

Below are links to some resources related to the topics we will cover.

---

Lambda Calculus

• Paul Levy's Lambda Calculus Notes
• Herman Geuvers's Notes on Lambda Calc and Types: notes, exercises, slides 1, slides 2, slides 3, slides 4
• Webapp/tutorial on reducing lambda terms

Type Theory

• Andreas Abel's short course
• Thorsten Altenkirch's short course
• Introduction to computational logic (downloadable)

Agda

• Verified functional programming in Agda (book), Aaron Stump.
• Dependent Types at Work, introductory tutorial by Ana Bove and Peter Dybjer.
• 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

Coq

• Getting Started: Introductory video tutorials
• Software Foundations, tips from OPLSS
• 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.
• Programs and Proofs: mechanizing math with dependent types
• Type theory and Coq (course) Radboud University, NL.
• UniMath Coq Library for univalent foundations, Voevodsky, et al.

---

Other resources

• CMSC 336: Type Systems for Programming Languages
• TypeFunc Resource Repository
• Notes from Types Summer School

---