Skip to content

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

Notifications You must be signed in to change notification settings

jsiek/B522-PL-Foundations

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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)

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

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

  • 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)

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

About

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

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages