B522-PL-Foundations

Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

View the Project on GitHub jsiek/B522-PL-Foundations

B522 Programming Language Foundations

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.

Instructor

Prof. Jeremy Siek, Luddy 3016, jsiek@indiana.edu

Lectures

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

Office Hours (in Luddy Hall 3016 or the neighboring 3014)

Assignments

  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.

Project, due May 1

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:

Ideas for project language features:

Schedule

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

Resources