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, [email protected]

Monday and Wednesday at 4:30-5:45pm in Luddy Hall Room 4101.

• Monday 3:00-4:30pm
• Tuesday 11:00-12:30pm
• Friday 1:30-3:00pm

1. January 20: Exercises Bin (in Naturals) and Bin-laws (in Induction).

2. January 27: Exercises Bin-predicates (in Relations) and Bin-embedding (in Isomorphism).

3. February 3: Exercises ⊎-weak-× (in Connectives), ⊎-dual-× (in Negation), ∃-distrib-⊎, ∃¬-implies-¬∀, Bin-isomorphism (in Quantifiers).

4. February 10: Exercises _<?_, iff-erasure (in Decidable), foldr-++, foldr-∷, and Any-++-⇔ (in Lists).

5. February 17: Exercises mul, —↠≲—↠′, and ⊢mul (in Lambda). Exercises progress′ and unstuck (in Properties).

6. 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.

7. 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.

8. March 13: do the variants exercise in Subtyping and Records.

9. March 30: do the products exercise in Bisimulation and the big-alt-implies-multi exercise in BigStep.

10. 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.

11. 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

• small-step reduction with evaluation contexts
• big-step semantics
• definitional interpreter (recursive function with gas)
• abstract machine (e.g. CEK)
• virtual machine (CAM)
• denotational semantics
• axiomatic semantics (e.g. Hoare Logic)

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:

• Lazy evaluation (aka. call-by-need) (e.g., see my paper Improving the lazy Krivine machine)
• Let polymorphism (extend TypeInference)
• Continuations (PLLC)
• Featherweight Java (TAPL Chapter 19)
• Exceptions (TAPL Chapter 14)
• While loops and variable assignment (the IMP language in FSPL)
• Recursive Types (TAPL Chapter 20)
• Nondeterminism
• Parallelism
• Reasoning about program equality using logical relations (PFPL)
• Bounded Quantification (TAPL Chapter 26)
• Higher-Order Polymorphism (TAPL Chapter 30)

• Join the course mailing list on Piazza.

• Join the PLFA mailing list plfa-interest and ask questions!

• Crash Course on Notation in Programming Language Theory