Schedule for Spring 2015

Advanced Programming Languages meets 10:10-11:00 on MWF in 219 Phillips Hall.

DateTopicNotesAssignments
Week 1
Jan 21 Goals of the Course
Operational Semantics
Introduction for functional languages

Lecture 1 Notes

Jan 23 Lambda Calculus
Operator Notation

Lecture 2 Notes

Week 2
Jan 26 More Lambda Calculus
Capture
Values

Lecture 3 Notes

Problem Set 1
Please submit homework through CMS.
Jan 28

Capture and Substitution
Lambda Theory

Lecture 4 Notes

Jan 30

Evaluators
Combinators

Lecture 5 Notes

Week 3
Feb 2

Lazy computation

Lecture 6 Notes
Equality in Lazy Computation Systems, Douglas Howe

Feb 4

Induction
More on combinators

Lecture 7 Notes

Feb 6

Partial recursive functions
Primitive recursion

Lecture 8 Notes

Week 4
Feb 9

Primitive recursive functions

Lecture 9 Notes
Primitive Recursion Examples

Problem Set 2
Feb 11

Intro to Coq

Lecture 10 Slides
Coq Examples

Feb 13

Scoping
Environment
Closures

Lecture 11 Notes
Week 5
Feb 16

No class: February break

Feb 18

Object language
Simple evaluator
CPS transformation
Defunctionalization
Abstract State Machine

Lecture 12 Notes
Includes topics from Lecture 14
Feb 20

Recursive function classes
Primitive recursion

Lecture 13 Notes
Week 6
Feb 23

Object language
Simple evaluator
CPS transformation
Defunctionalization
Abstract State Machine

Lecture 14 Notes
Includes topics from Lecture 12
Feb 25

Abstract State Machines
Kleene's Normal Form Theorem

Lecture 15 Notes
Introduction to Metamathematics, p.270-275, S.C Kleene, 1971
Feb 27

Applied lambda calculus
Kleene's Normal Form Theorem
Abstract approach to PLs

Lecture 16 Notes
A formal proof of Borodin-Trakhtenbrot's Gap Theorem, Andrea Asparti, 2013.
Week 7
March 2

Church Rosser Theorem
Typed lambda calculus
Review

Lecture 17 Notes
Additional notes from Dr. Rahli
March 4

Typed lambda calculus
Statman's Theorem
Partial types
Review

Lecture 18 Notes
March 6

Prelim Exam

Week 8
March 9

Prelim Review
Answers to Midterm Exam

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
Recursive number theory
Goodstein's rules for reasoning

Lecture 22 NotesProblem Set 3
Hints for problem 2
March 18

Partial Recursive Functions
Kleene's recursion theorem

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
Least Upper Bound Theorem
Constructive PCF

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
Blum Size 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
Operational Semantics
Evaluation of Commands

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
Hoare rules and logic

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
Constructive 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
Quotient type
Propositions-as-types

Lecture 37 Notes
May 1

Propositions-as-types

Lecture 38 Notes
Week 16
May 4

Complete induction
Final exam notes

Lecture 39 Notes
The Basic Nuprl Type Theory, Christoph Kreitz.
May 6

Propositions-as-types
Classical logic

Lecture 40 Notes