Principles of Programming Languages Concentration

This concentration is available to SCS students only.

Robert Harper, Concentration Director and Advisor (GHC 9229)

Programming languages play a central role in computer science. All programs are written in a language, and it is obvious that some are better than others, at least for some purposes. The constant demand for new languages reflects the changing demands for constructing reliable and maintainable software systems. Academic research in programming language principles has led to numerous advances in language design, language implementation, and program verification intended to meet these changing expectations through the development of a rigorous theory of programming languages.

Carnegie Mellon is a recognized leader in programming languages, characterized by a strong emphasis on the centrality of type theory, a consolidation of ideas in mathematical semantics, programming logics, and programming language design and implementation. The purpose of the PoPL concentration is to teach the comprehensive view of the field that has been developed here over many decades. Type theory teaches how to define a language, and how to show that it is well-defined, free of internal contradictions. It teaches the mathematical foundations for abstraction and modularity, concepts that are fundamental to building maintainable systems. It teaches how to use a rigorous language definition as the basis for building a compiler that correctly implements the definition, and provides the tools necessary to achieve it. It teaches the logical foundations of program development, how to precisely specify the intended behavior of a program, and how to use machine tools to verify that a program meets those expectations. It gives precise meaning to language concepts, relating them to one another, and distinguishing concepts that are often confused or conflated. It teaches how to specify and verify the resource usage of a program (such as its sequential and parallel time and space complexity) without resorting to a model of how it is implemented on a machine; it supports using actual code, rather than pseudo-code, for defining and analyzing algorithms.

The PoPL concentration is of value to a broad range of students. For the practically minded it will provide the foundation for structuring and validating programs, using type systems or more advanced forms of specification. For the theoretically minded it will provide the foundation for understanding the close relationship between specification and programs on one hand and mathematical conjecture and proof on the other. The elegance of the PoPL lies in their unification of these two perspectives: the theory applies directly to the practice, and the practice informs the theory.

Learning Objectives

The PoPL concentration is characterized by a collection of learning outcomes that it seeks to achieve. These may be summarized by the knowledge that
students may expect to gain by concentrating in the area. By their choice of electives each student will choose an emphasis within the area; the required courses ensure that this includes at least the first five objectives:

  • Specify the concrete and abstract syntax of a programming language, including a precise specification of the binding and scope of declarations.
  • Define the static semantics (compile-time constraints) of a programming language using typing judgments, and how to state and prove that it properly defined.
  • Define the dynamics semantics (run-time behavior) of a language using operational and denotational methods.
  • Verify rigorously that the statics and dynamics of a language are coherent, a property commonly called type safety.
  • Understand the propositions-as-types principle, which relates programs to proofs and specifications to theorems, and know how to apply it in language design and program verification.
  • Formulate type and assertion languages for specifying the behavior of a program, and how to verify that a program satisfies such a specification.
  • Specify the cost (sequential and parallel time and space complexity) for a program written in a precisely defined language, and how to verify that a given program meets stated cost bounds.
  • Use software tools to verify both the properties of languages and the specifications of programs written in well-defined languages.
  • Use the static and dynamic semantics of a language to derive a compiler for it that complies with these definitions, and how to use types and verification tools to ensure compiler correctness.
  • Relate a language definition to its implementation, both in terms of the run-time structures required, but also to validate abstract cost measures in an implementation.

Prerequisites

This concentration requires students to complete the following courses before the concentration can be completed:

15-122 Principles of Imperative Computation 10
15-150 Principles of Functional Programming 10
15-151 Mathematical Foundations for Computer Science 10
15-210 Parallel and Sequential Data Structures and Algorithms 12
15-213 Introduction to Computer Systems 12
15-251 Great Ideas in Theoretical Computer Science 12

Course Requirements

This concentration requires two courses along with two additional electives. 

Required Courses (complete all of the following):

15-312 Foundations of Programming Languages 12
15-317 Constructive Logic 9

Electives (complete two of the following):

15-314 Programming Language Semantics 12
15-316 Software Foundations of Security and Privacy 9
15-414 Bug Catching: Automated Program Verification 9
15-417 HOT Compilation 12
15-424 Logical Foundations of Cyber-Physical Systems 12
Any graduate-level Programming Languages course(s), with prior permission of the concentration advisor and the course instructor(s).

Students may use one semester of a senior thesis supervised by a member of the Principles of Programming faculty in the Computer Science Department as a replacement for one of the two electives.

Transfer of credit for courses taken outside of Carnegie Mellon University toward this concentration will not be allowed.

Double Counting

Either 15-312 or 15-317 (but not both) may be double counted towards any major, minor or other concentration being pursued by the student. No other double counting is permitted.

Advising and Management

Participation in this concentration is supervised by the concentration coordinator in cooperation with the students academic advisor, course instructors, and, as appropriate, thesis supervisor. The current coordinator is Robert Harper. Content for this concentration will be reviewed yearly by the Principles of Programming faculty in the Computer Science Department. 

Students interested in pursuing this concentration should contact Robert Harper for an initial advising consultation.