Carnegie Mellon University

15-814 (Type Systems for Programming Languages)

Classes will not begin until after the CSD Immigration Course

This is an introductory course on the foundations of programming languages. The central organizing principle of language design is the identification of language features with types. The theory of programming languages, therefore, reduces to the theory of types. Type theory is a comprehensive foundational theory of computation. Type theory has its orgins in proof theory (the theory of human reason) and is closely related to category theory (the general theory of mathematical structures). The tripartite relationship between type theory, proof theory, and category theory is fundamental to the study of programming languages. We will place special emphasis on the propositions-as-types correspondence, in which programs of a type are identified with proofs of the corresponding proposition. (Similar correspondences hold between type theory and category theory (types are objects, programs are maps) and between category theory and proof theory (propositions are objects, proofs are maps), but we shall not consider these in this course.)

Please refer to "" this link for the most recent schedule updates.