Indiana University, Spring 2026
In this course we learn how to write mechanized proofs in Agda of theorems about programming languages. The course will use the online textbook Programming Language Foundations in Agda (PLFA).
Agda is a proof assistant and a dependently typed language. No prior knowledge of Agda is assumed; it will be taught from scratch. Prior knowledge of another proof assistant or dependently typed language is helpful but not necessary.
Prof. Jeremy Siek, Luddy 3016, jsiek@iu.edu
Tuesday and Thursday at 2:20-3:35pm in Wylie Hall (WY) Room 101.
January 20, Exercises Bin (in Naturals) and
Bin-laws (in Induction).
Exercises Bin-predicates (in Relations) and
Bin-embedding (in Isomorphism).
Exercises
⊎-weak-× (in Connectives),
⊎-dual-× (in Negation),
∃-distrib-⊎,
∃¬-implies-¬∀,
Bin-isomorphism (in Quantifiers).
Exercises
_<?_,
iff-erasure (in Decidable),
foldr-++,
foldr-∷, and
Any-++-⇔ (in Lists).
Exercises
mul,
—↠≲—↠′, and
⊢mul
(in Lambda).
Exercises
progress′ and
unstuck
(in Properties).
Formalize the STLC using the extrinsic
style, as in Lambda,
but using de Bruijn indices to represent variables,
as in DeBruijn.
You should use the ext, rename, exts, and subst
functions from the DeBruijn chapter, simplifying the
type declarations of those functions. For example,
exts : ∀ {Γ Δ}
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
---------------------------------
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
becomes
exts :
→ (Var → Term)
------------
→ (Var → Term)
where Var is define to just be ℕ.
You will need to prove a type preservation lemma for
each of ext, rename, exts, and subst,
whose declaration will be analogous to the type
declaration of those functions in the DeBruijn chapter.
For example,
exts-pres : ∀ {Γ Δ σ}
→ (∀ {A x} → Γ ∋ x ⦂ A → Δ ⊢ σ x ⦂ A)
----------------------------------------------------
→ (∀ {A B x} → Γ , B ∋ x ⦂ A → Δ , B ⊢ (exts σ) x ⦂ A)
Prove the analogous theorem to preserve
in Properties.
You may omit natural numbers (0, suc, and case) and μ
from your formalization of the STLC, instead
including a unit type.
Termination and Bidirectional Typing:
Extend the termination proof for STLC to include products and sums, as they appear in Chapter More (you may use either approach to products). Also, try to add μ and report on where the proof breaks.
Extend the bidirectional type rules, synthesize, and inherit
to handle products and sums.
Do the variants exercise in
Subtyping and Records.
Do the products exercise in
Bisimulation
and the big-alt-implies-multi exercise
in BigStep.
Project Description Due. Write 1 page describing your project. The description should include a list of the formal artifacts (definitions, theorems) that you plan to turn in.
Choose a language feature that is not spelled out in PLFA to formalize and prove type safe in Agda. (If you have a different kind of project in mind, I’m happy to consider alternatives, so long as it includes proving some non-trivial property of a programming language.) Your formalization should include both a static semantics (aka. type system), a dynamic semantics, and a proof of type safety. For the dynamic semantics you must use a different style than the approach used in PLFA, that is, do not use a reduction semantics. Examples of other styles you can use are
Resources:
The book Types and Programming Languages (TAPL) by Benjamin Pierce has many examples of language features that would be an appropriate choice for your project.
The book Semantics Engineering with PLT Redex by Felleisen, Findler, and Flatt is a good resource for evaluation contexts, abstract machines, and continuations. The earlier book draft Programming Languages and Lambda Calculi (PLLC) by Felleisen and Flatt covers similar material.
The Formal Semantics of Programming Languages (FSPL) by Winskel includes lots of semantics styles (small-step, big-step, axiomatic, denotational), eager and lazy evaluation, nondeterminism and parallelism.
Practical Foundations for Programming Languages (PFPL) by Robert Harper includes material on logical relations.
Type Safety in Three Easy Lemmas is a blog post of mine that shows how to prove type safety using a definitional interpreter with gas.
Type Safety in Five Easy Lemmas is a blog post of mine that shows how to prove type safety using an abstract machine.
Ideas for project language features:
| Month | Day | Topic |
|---|---|---|
| January | 13 | Naturals & Induction |
| 15 | Relations | |
| 20 | Equality & Isomorphism (unusual day, regular time) | |
| 22 | Connectives & Negation | |
| 27 | Quantifiers & Decidable | |
| 29 | Lists and higher-order functions | |
| February | 3 | Lambda the Simply Typed Lambda Calculus |
| 5 | Properties such as type safety | |
| 10 | DeBruijn representation of variables | |
| 12 | More constructs: numbers, let, products (pairs), sums, unit, empty, lists | |
| 17 | STLC Termination via Logical Relations | |
| 19 | Inference bidirectional type inference | |
| 24 | Subtyping and Records | |
| 26 | Bisimulation | |
| March | 3 | Untyped Lambda Calculus |
| 5 | Confluence of the Lambda Calculus | |
| 10 | BigStep Call-by-name Evaluation of the Lambda Calculus | |
| 12 | Spring Break, no class | |
| 17 | Spring Break, no class | |
| 19 | Denotational semantics of the Lambda Calculus | |
| 24 | Denotational continued, Recording | |
| 26 | Compositional | |
| 31 | Soundness, Recording | |
| April | 2 | Adequacy, Recording |
| 7 | ContextualEquivalence and ScottNumeralsPlus, Recording | |
| 9 | Unification, Recording | |
| 14 | Unification continued, Recording | |
| 16 | TypeInference, Recording | |
| 21 | Gradual Typing, Recording | |
| 23 | SystemF Universal Types (aka. parametric polymorphism), Recording | |
| 28 | TBD | |
| 30 | TBD |