include_once "6110header.php"; ?>
Advanced Programming Languages meets 10:10-11:00 on MWF in 219 Phillips Hall.
Date | Topic | Notes | Assignments |
---|---|---|---|
Week 1 | |||
Jan 21 | Goals of the Course Operational Semantics Introduction for functional languages |
||
Jan 23 | Lambda Calculus Operator Notation |
||
Week 2 | |||
Jan 26 | More Lambda Calculus Capture Values |
Problem Set 1
Please submit homework through CMS. |
|
Jan 28 | Capture and Substitution |
||
Jan 30 | Evaluators |
||
Week 3 | |||
Feb 2 | Lazy computation |
Lecture 6 Notes | |
Feb 4 | Induction |
||
Feb 6 | Partial recursive functions |
||
Week 4 | |||
Feb 9 | Primitive recursive functions |
Problem Set 2 | |
Feb 11 | Intro to Coq |
||
Feb 13 | Scoping | Lecture 11 Notes | |
Week 5 | |||
Feb 16 | No class: February break | ||
Feb 18 | Object language |
Lecture 12 Notes Includes topics from Lecture 14 | |
Feb 20 | Recursive function classes | Lecture 13 Notes | |
Week 6 | |||
Feb 23 | Object language | Lecture 14 Notes Includes topics from Lecture 12 | |
Feb 25 | Abstract State Machines | Lecture 15 Notes Introduction to Metamathematics, p.270-275, S.C Kleene, 1971 | |
Feb 27 | Applied lambda calculus | Lecture 16 Notes A formal proof of Borodin-Trakhtenbrot's Gap Theorem, Andrea Asparti, 2013. | |
Week 7 | |||
March 2 | Church Rosser Theorem | Lecture 17 Notes Additional notes from Dr. Rahli | |
March 4 | Typed lambda calculus | Lecture 18 Notes | |
March 6 | Prelim Exam | ||
Week 8 | |||
March 9 | Prelim Review |
Midterm answers Answers were given to the ten short answer questions. Nearly all students answered the second and third questions correctly. | |
March 11 | Expressing mathematics in PL | Lecture 20 Notes Recursive Number Theory, R. L. Goodstein, 1957. | |
March 13 | Intro to Proving in Coq | Lecture 21 Notes Coq source file | |
Week 9 | |||
March 16 | Equational reasoning | Lecture 22 Notes | Problem Set 3 Hints for problem 2 |
March 18 | Partial Recursive Functions | Lecture 23 Notes Partial Recursive Functions, from Introduction to Metamathematics, Kleene | |
March 20 | Kleene's generalized recursion theorem | Lecture 24 Notes | |
Week 10 | |||
March 23 | Lambda decidability | Lecture 25 Notes Computational foundations of basic recursive function theory, R.L. Constable and S. Smith, 1993. | |
March 25 | LCF/PCF/CBRFT Theorem and results | Lecture 26 Notes | |
March 27 | Rice's Theorem | Lecture 27 Notes On the Size of Machines, Manuel Blum, 1967. Look particularly at this from Blum The Recursion Theorem, Kleene. | |
Week 11 | |||
March 30-
April 3 |
Spring Break, no class | ||
Week 12 | |||
April 6 | Blum Size Theorem continued | Lecture 28 Notes
Introduction to operational semantics, from "The Formal Semantics of Programming Languages: An introduction", Glynn Winskel, 1993. | |
April 8 | IMP | Lecture 29 Notes Techniques for recursion, from "The Formal Semantics of Programming Languages: An Introduction", Glynn Winskel, 1993. | PS4, due Fri. April 24 |
April 10 | Semantics for IMP | Lecture 30 Notes Hoare rules, from "The Formal Semantics of Programming Languages: An Introduction", Glynn Winskel, 1993. | |
Week 13 | |||
April 13 | Hoare axioms | Lecture 31 Notes
PLVC2 Programming logic, from PLCV2 Programming Logic, Lecture Notes in Computer Science, v.135, p.83, R. L. Constable, S.D Johnson, and C.D. Eichenlaub, 1982. Hoare rules, from "The Formal Semantics of Programming Languages: An Introduction", Glynn Winskel, 1993. | |
April 15 | Fixed point induction | Lecture 32 Notes | |
April 17 | Introduction to Loop language | Lecture 33 Notes PLCV2 Programming Logic, Lecture Notes in Computer Science, v.135, pp.23-32, R. L. Constable, S.D Johnson, and C.D. Eichenlaub, 1982. Computational Complexity and Program Structure, A.R. Meyer and D.M. Ritchie, IBM Research, 1967. | |
Week 14 | |||
April 20 | Hoare axioms | Lecture 34 Notes
A Critique of the Foundations of Hoare-Style Programming Logics, Michael O'Donnell, Technical Report, Purdue University, 1980. | |
April 22 | Constructive type theory | Lecture 35 Notes
The Basic Nuprl Type Theory, Christoph Kreitz. The Triumph of types: Principia Mathematica's Impact on Computer Science, Robert Constable. | |
April 24 | Type theory | Lecture 36 Notes The Brouwer-Hilbert Controversy, from Brouwer's Intuitionism, Vol. 2, pg. 100-103, W.P. van Stigt, 1990. | |
Week 15 | |||
April 27 | No class - Charter Day | The Unlimited Register Machine from Computability: An Introduction to recursive function theory,pp. 8-13, N.J. Cutland, 1980. Turing Machines, from Formal Languages and Their Relation to Automata, pp. 80-83, John E. Hopcroft an Jeffrey D. Ullman, 1969. Derivation of a Fast Integer Square Root Algorithm, Christoph Kreitz. | Problem Set 5 |
April 29 | Universes | Lecture 37 Notes | |
May 1 | Propositions-as-types | Lecture 38 Notes | |
Week 16 | |||
May 4 | Complete induction | Lecture 39 Notes
The Basic Nuprl Type Theory, Christoph Kreitz. | |
May 6 | Propositions-as-types | Lecture 40 Notes |