plclub/cis670-16fa
Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016
{ "createdAt": "2016-08-30T12:03:13Z", "defaultBranch": "master", "description": "Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016", "fullName": "plclub/cis670-16fa", "homepage": null, "language": "Coq", "name": "cis670-16fa", "pushedAt": "2022-10-25T19:11:40Z", "stargazersCount": 42, "topics": [], "updatedAt": "2024-11-11T21:56:16Z", "url": "https://github.com/plclub/cis670-16fa"}Advanced Topics in Programming Languages
Section titled “Advanced Topics in Programming Languages”CIS 670, Fall 2016
Section titled “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
Section titled “Schedule”| Date | Speaker | Lecture Topic | Notes |
|---|---|---|---|
| 8/30 | Stephanie | Intros, Locally nameless | [083016.md]!(notes/083016.md) |
| 9/1 | Stephanie | Ch 2 - Abstract binding trees | [090116.md]!(notes/090116.md) |
| 9/6 | Stephanie | Cofinite quantification | [090616.md]!(notes/090616.md) |
| 9/8 | Stephanie | Ch 4 - Structural rules | [090816.md]!(notes/090816.md) |
| 9/13 | Stephanie | Ch 4 & 5 - More typing & evaluation | [091316.md]!(notes/091316.md) |
| 9/15 | Stephanie | Ch 6 & 7 - Type soundness times 2 | [091516.md]!(notes/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]!(code/Ch9.v) |
| 9/27 | Solomon (smaina) | Ch 10 - Product Types | [092716.md]!(notes/092716.md) |
| 9/29 | Yao (liyao) | Ch 11 - Sum Types | [092916.md]!(notes/092916.md) |
| 10/4 | Pritam (pritam) | Ch 12 - Constructive Logic | [100416.md]!(notes/100416.md) [slides]!(notes/IntuitionisticPropositionalLogicLecture.pdf) |
| 10/6 | Fall break (no class) | ||
| 10/11 | Antoine (voizard) | Ch 13 - Classical Logic | [101116.md]!(notes/101116.md) |
| 10/13 | Leo (llamp) | Ch 14 - Generic Programming | [101316.md]!(notes/101316.md) |
| 10/18 | Nicholas (chkoh) | Ch 15 - Inductive and Coinductive Types | [101816.md]!(notes/101816.md) |
| 10/20 | Yishuai (yishuai) | Ch 16 - System F of Polymorphic Types | [102016.md]!(notes/102016.md) |
| 10/24 | Teng (tengz) | Ch 17 - Abstract Types | [102516.md]!(notes/102516.md) [code]!(code/abstractTypeExample.v) |
| 10/27 | Richard (rmzhang) | Ch 19 - System PCF of Recursive Functions | [102716.md]!(notes/102716.md) |
| 11/1 | Stephanie | Ch 20 - System FPC of Recursive Types | [110116.md]!(notes/110116.md) |
| 11/3 | Kenny (kfoner) | Ch 21 - The Untyped lambda-Calculus | [110316.md]!(notes/110316.md) [code]!(code/Ch21.hs) |
| 11/8 | Omar (omarsa) | Ch 22 - Dynamic Typing | [110816.md]!(notes/110816.md) [code]!(code/dynamicTyping.clj) |
| 11/10 | Hengchu (hengchu) | Ch 23 - Hybrid Typing | [111016.md]!(notes/111016.md) |
| 11/15 | Stephanie | Ch 46 - Equality for System T | [111516.md]!(notes/111516.md) [code]!(code/Ch46.v) |
| 11/17 | Stephanie | Ch 46 cont. | |
| 11/22 | Stephanie | Ch 48 - Parametricity | [112216.md]!(notes/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
Section titled “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)