cty12/b522-pl-foundations

Course Webpage for B522 Programming Language Foundations, Spring 2020, Indiana University

B522 Programming Language Foundations

Indiana University, Spring 2020

In this course we study the mathematical foundations of programming languages. That is, how to define programming languages and how to reason about those languages and programs written in them. The course will use the online textbook

Programming Language Foundations in Agda (the beta version)

Agda is a proof assistant and a dependently typed language. No prior knowledge of Agda is assumed; it will be taught from scratch. Prior knowledge of another proof assistant or dependently typed language is helpful but not necessary.

Instructor

Prof. Jeremy Siek, Luddy 3016, [email protected]

Lectures

Monday and Wednesday at 4:30-5:45pm in Luddy Hall Room 4101.

Office Hours (in Luddy Hall 3016 or the neighboring 3014)

• Monday 3:00-4:30pm
• Tuesday 11:00-12:30pm
• Friday 1:30-3:00pm

Assignments

• January 20: Exercises Bin (in Naturals) and Bin-laws (in Induction).

• January 27: Exercises Bin-predicates (in Relations) and Bin-embedding (in Isomorphism).

• February 3: Exercises ⊎-weak-× (in Connectives), ⊎-dual-× (in Negation), ∃-distrib-⊎, ∃¬-implies-¬∀, Bin-isomorphism (in Quantifiers).

• February 10: Exercises _<?_, iff-erasure (in Decidable), foldr-++, foldr-∷, and Any-++-⇔ (in List).

Schedule

Month	Day	Topic
January	13	Naturals & Induction
	15	Relations
	16	Equality & Isomorphism (unusual day, regular time)
	27	Connectives & Negation
	28	Quantifiers & Decidable (unusual day, regular time)
	29	Lists and higher-order functions
February	3	Lambda the Simply Typed Lambda Calculus
	5	Properties such as type safety
	10	DeBruijn representation of variables
	12	More constructs: numbers, let, products (pairs), sums, unit, empty, lists
	17	Inference bidirectional type inference
	19	Untyped Lambda Calculus
	24	Confluence of the Lambda Calculus
	26	BigStep Call-by-name Evaluation of the Lambda Calculus
March	2	Denotational semantics of the Lambda Calculus
	4	Compositional
	9	Soundness
	11	Adequacy
	16	ContextualEquivalence
	18	References and the Heap
	23	Subtyping and Records
	25	Classes and Objects (Featherweight Java)
	30	Gradual Typing
April	1	Universal and Existential Types (Parametric Polymorphism)
	6	Hindley-Milner Inference
	8	Recursive Types
	13	Intersection and Union Types
	15	Higher-Order Polymorphism
	20	Dependent Types
	22	TBD
	27	TBD
	29	TBD

Resources

• Join the course mailing list on Piazza.

• Join the PLFA mailing list plfa-interest and ask questions!

• Crash Course on Notation in Programming Language Theory