Theories of Programming Languages Fall 2012, University of Science and Technology of China

Reading Materials

Why study programming languages?

• Robert Harper's article Why Study Programming Languages?

The Coq proof assistant

• Webpage of Coq
• Reference Manual and Standard Library
• A tutorial on Coq, and A tutorial on recursive types in Coq
• Teach materials in 3rd Coq Summer School

Lambda Calculus

• Peter Selinger's Lecture Notes on the Lambda Calculus (a local copy)

Curry-Howard Isomorphism

• Phil Wadler's Proofs are Programs: 19th Century Logic and 21st Century Computing (a local copy and a talk)