Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016
Coq Haskell HTML TeX Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
code
notes
projects
.gitignore
.gitmodules
LICENSE
README.md

README.md

Advanced Topics in Programming Languages

CIS 670, Fall 2016

Instructor: Stephanie Weirich
Time: TR 1:30-3PM
Location: Towne 319
Textbook: Practical Foundations for Programming Languages
Prerequisite: CIS 500 or PhD student status

Schedule

Date Speaker Lecture Topic Notes
8/30 Stephanie Intros, Locally nameless 083016.md
9/1 Stephanie Ch 2 - Abstract binding trees 090116.md
9/6 Stephanie Cofinite quantification 090616.md
9/8 Stephanie Ch 4 - Structural rules 090816.md
9/13 Stephanie Ch 4 & 5 - More typing & evaluation 091316.md
9/15 Stephanie Ch 6 & 7 - Type soundness times 2 091516.md
9/20 ICFP (no class) Ch 8 - Function Definitions and Values read on your own
9/22 ICFP (no class) Ch 9 - System T of Higher-Order Recursion finish Ch9.v
9/27 Solomon (smaina) Ch 10 - Product Types 092716.md
9/29 Yao (liyao) Ch 11 - Sum Types 092916.md
10/4 Pritam (pritam) Ch 12 - Constructive Logic 100416.md slides
10/6 Fall break (no class)
10/11 Antoine (voizard) Ch 13 - Classical Logic 101116.md
10/13 Leo (llamp) Ch 14 - Generic Programming 101316.md
10/18 Nicholas (chkoh) Ch 15 - Inductive and Coinductive Types 101816.md
10/20 Yishuai (yishuai) Ch 16 - System F of Polymorphic Types 102016.md
10/24 Teng (tengz) Ch 17 - Abstract Types 102516.md code
  |                     |                                            | Project Checkpoint due

10/27 | Richard (rmzhang) | Ch 19 - System PCF of Recursive Functions | 102716.md 11/1 | Stephanie | Ch 20 - System FPC of Recursive Types | 110116.md 11/3 | Kenny (kfoner) | Ch 21 - The Untyped lambda-Calculus | 110316.md code 11/8 | Omar (omarsa) | Ch 22 - Dynamic Typing | 110816.md code 11/10 | Hengchu (hengchu) | Ch 23 - Hybrid Typing | 111016.md 11/15 | Stephanie | Ch 46 - Equality for System T | 111516.md code 11/17 | Stephanie | Ch 46 cont. | 11/22 | Stephanie | Ch 48 - Parametricity | 112216.md 11/24 | Thanksgiving (no class) 11/29 | Project demos (Richard, Hengchu, Teng) | 12/1 | Project demos (Nicolas, Yishuai, Solomon) | | Yishuai 12/6 | Project demos (Omar, Leo & Kenny) | 12/8 | Project demos (Pritam, Antoine, Yao) |

Potential topics from PFPL

  • Part I Judgements and Rules (Stephanie)
  • Part II Statics and Dynamics (Stephanie)
  • Part III Total Functions (Read on your own)
  • Part IV Finite Data Types (Solomon Ch10, Yao Ch11)
  • Part V Types and Propositions (Pritam Ch12, Antoine Ch13)
  • Part VI Infinite Data Types (Kenny Ch14, Nicolas Ch15)
  • Part VII Variable Types (Yishuai Ch16, Teng Ch17, skip Ch18?)
  • Part VIII Partiality and Recursive Types (Richard Ch19 & Stephanie Ch20)
  • Part IX Dynamic Types (Leo Ch21, Omar Ch22, Hengchu Ch23)

Resources