Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University
Indiana University, Spring 2020
In this course we study the mathematical foundations of programming languages. That is, how to define programming languages and how to reason about those languages and programs written in them. The course will use the online textbook
Programming Language Foundations in Agda (PLFA) (the beta version)
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@indiana.edu
Monday and Wednesday at 4:30-5:45pm in Luddy Hall Room 4101.
January 20: Exercises Bin
(in Naturals) and
Bin-laws
(in Induction).
January 27: Exercises Bin-predicates
(in Relations) and
Bin-embedding
(in Isomorphism).
February 3: Exercises
⊎-weak-×
(in Connectives),
⊎-dual-×
(in Negation),
∃-distrib-⊎
,
∃¬-implies-¬∀
,
Bin-isomorphism
(in Quantifiers).
February 10: Exercises
_<?_
,
iff-erasure
(in Decidable),
foldr-++
,
foldr-∷
, and
Any-++-⇔
(in Lists).
February 17: Exercises
mul
,
—↠≲—↠′
, and
⊢mul
(in Lambda).
Exercises
progress′
and
unstuck
(in Properties).
February 28: 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.
March 6:
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.
March 13: do the variants
exercise in
Subtyping and Records.
March 30: do the products
exercise in
Bisimulation
and the big-alt-implies-multi
exercise
in BigStep.
April 3: 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.
April 10: do the denot-plusᶜ
and denot-church
in Denotational.
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 | |
16 | Equality & Isomorphism (unusual day, regular time) | |
27 | Connectives & Negation | |
28 | Quantifiers & Decidable (unusual day, regular time) | |
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 | 2 | Untyped Lambda Calculus |
4 | Confluence of the Lambda Calculus | |
9 | BigStep Call-by-name Evaluation of the Lambda Calculus | |
11 | Denotational semantics of the Lambda Calculus | |
16 | Spring Break, no class | |
18 | Spring Break, no class | |
23 | More Spring Break, no class | |
25 | More Spring Break, no class | |
30 | Denotational continued, Recording | |
April | 1 | Compositional (forgot to push record!) |
6 | Soundness, Recording | |
8 | Adequacy, Recording | |
13 | ContextualEquivalence and ScottNumeralsPlus, Recording | |
15 | Unification, Recording | |
20 | Unification continued, Recording | |
22 | TypeInference, Recording | |
27 | Gradual Typing, Recording | |
29 | SystemF Universal Types (aka. parametric polymorphism), Recording |
Join the course mailing list on Piazza.
Join the PLFA mailing list plfa-interest and ask questions!