Skip to content

Latest commit

 

History

History
62 lines (43 loc) · 1.96 KB

083016.md

File metadata and controls

62 lines (43 loc) · 1.96 KB
Raw

August 30, 2016

To Read: Chapters 1,2 & 4 of PFPL

To Do:

  • Install Coq and Metalib
  • Complete Ch4.v

Introduction and course goals

Goal: extend & deepen knowledge of programming language theory and types Provide a firm foundation for the sorts of proofs that appear in PL research papers, such as in POPL and ICFP.

Focus: type abstraction and equality in typed lambda calculi

References: Bob Harper's Practical Foundations for Programming Languages (possibly) Appel's Verified Functional Algorithms

Nonfocus: program verification, dependent types

Background

Everyone in here should either be a PhD student or have taken CIS 500. In general, we expect that you have experience with functional programming (OCaml or ML), and have seen a type safety proof for simply-typed lambda calculus.

Although we'll start with some mechanical proofs in Coq, Coq experience is useful but not required.

Who here has:

  • taken CIS 500 at Penn?
  • self-studied SF (or as part of a class)?
  • taken another course on PL theory?
  • Used Coq before?

What you should expect this semester

  • If you are taking this class for a grade

    • Come to every class prepared (I'll announce the reading for the next class ahead of time)
    • You must send me 1-2 questions the morning before each class (via email)
    • Be prepared to give one lecture this semester on a chapter in PFPL
    • A few homework assignments at the beginning of the semester to make sure everyone is up to speed
    • Semester project (in groups) to go deeper on a particular topic
    • replicate the proofs in a classic paper (by hand or in Coq)
    • extend a classic paper with a new feature
    • some other exploration

  • If you are auditing this semester

    • Come to every class prepared (I'll announce the reading for the next class ahead of time)
    • Send me 1-2 questions before each class

First topic

Working with a model of a simple, typed programming language

See Ch4.v