This is a graduate course on the logical foundations and algorithmic techniques used to ensure that programs do what they are supposed to do. It focuses on two key aspects of automated reasoning:

1. Specification: logics to define the expected behavior of a program in a machine-readable form,
2. Verification: methods to automatically check if a program meets its specification.

The course explores both the theory and practice of automated computer-aided reasoning, and its application to reasoning about program behavior. This exploration covers a breadth of reasoning techniques and tools currently in use, e.g. SAT/SMT solvers, examining them from the both an implementation and user perspective.

This is a course on the principles of programming languages and their application. The emphasis is on ideas and techniques relevant to practitioners, but includes theoretical foundations crucial for deeper understanding: abstract syntax, formal semantics, type systems, and abstraction. Work in the course involves exploring programming languages and features as both a user (by writing programs in those languages) and a language designer (by implementing interpreters for various languages), and as a scholar (by proving mathematical properties of them). We will investigate language-based techniques for analyzing program behavior, and discuss what guarantees a programming language can provide its users about the abstractions it provides. The course will also offer some historical perspective on the evolution of programming languages and why some designs thrive while others fail. Upon successfully completing this course, students will be able to:

1. Write programs in two languages with state-of-the-art type systems, Rust and Haskell.
2. Compare and contrast different language-provided abstractions, including ad-hoc and parametric polymorphism, user-defined data types, and static and dynamic memory safety.
3. Precisely formulate the syntax and runtime behavior of a programming language.
4. Specify different notions of safety for a programming language and implement language-based techniques for ensuring the safety of programs.

The first half of the course will discuss these topics in the context of the (mostly) pure functional language, Haskell, while the second half will use the modern systems language Rust.

This course will examine the design and implementation of programming languages from a foundational perspective. Our goal will be to develop tools that will enable us to both design and specify new language features, to precisely understand the rationale for existing features in modern languages, and to understand how design decisions can impact implementations. The course will be divided into roughly three parts:

1. principles (e.g., semantics, type systems, specifications)
2. proof techniques and formal reasoning
3. automated theorem proving using the Coq proof assistant

Our discussion of principles will be crafted in the context of definitions and theorems that capture salient properties of modern languages. The validation of these theorems will be undertaken using Coq, a powerful theorem prover and mechanized proof assistant.

Over the last several decades, the programming languages and formal methods communities have made significant progress toward ensuring that a program is correct with respect to some \emph{specification} of its intended behavior, e.g. that an implementation of quicksort always returns a sorted list, a gradebook application correctly calculates the average test score, or that a program is free of any divide by zero errors. These communities have developed a number of techniques to automatically verify these sorts of properties, to the point that these techniques have been adopted to verify a wide variety of real-world systems, from device drivers at Microsoft, to absence of null pointer exceptions and concurrency bugs in Android and Java applications at Facebook.

The vast majority of these techniques deal with specifications of the behavior of a single execution of a program. Many desirable program behaviors fall outside this class, however, and require specifications that can describe multiple program executions. Somewhat surprisingly, examples of such relational properties or hyperproperties include foundational programming language concepts like parametricity, program refinement, and compiler correctness. Hyperproperties also abound in other computer science communities, including security ( absence of information leakeage) multiparty computation) databases (weak consistency), and AI (fairness, robustness).

This seminar will consider both the specification of a wide variety of hyperproperties, as well as the verification of programs with respect to relational specifications. Importantly, this class will strive to appreciate hyperproperties from the perspective of the communities that created them, in order to better connect them to a more PL/FM-view. To this end, the last fourth of the class will be an in-depth look at secure multiparty computation and how PL techniques for relational reasoning can be applied in that setting.

A student who successfully fulfills the course requirements will havethe ability to

• Architect and design quality software
• Contrast and critique software lifecycle models
• Create software using current software engineering tools, methods, and concepts
• .Work together on a team in a productive and professional manner
• Inspect and test software and documentatio

A key objective of this course is to give students hands-on experience in developing software as part of a team, following the scrum methodology. Teams will propose a project by developing a project charter and backlog. Subsequently, there will be three sprints, each preceded by a planning document and proceeded by a retrospective. A review will take place during each sprint wherein a project coordinator (teaching assistant) will assess the efforts and accomplishments of the team. There will be a final project presentation at the conclusion of the semester.

Imagine a world in which you could simply tell your computer what problem a program should solve and have it write the program for you. Freed from the humdrum tasks of coding, you would be able focus on finding the right problems to solve (while also having more time to drink coffee). This is the dream of program synthesis: to automatically build implementations from high-level description of a program.

This seminar will begin with a broad overview of the field, including:

1. how to learn a program from examples (inductive synthesis)
2. how users can guide the search for an implementation (deductive synthesis)
3. how to leverage cutting-edge theorem provers to find programs automatically

The second half of the course will focus on applications of synthesis to a variety of domains, including security, education, performance, and human computer interaction, with the specific topics tailored to participants' interests. Each unit will review the state of the art in the field with readings from the latest publications.

This course covers the basics of designing webpages using HTML, Javascript, and PHP, and connecting them to SQL database backends to allow for dynamic content. Students will learn the basics of each of these languages individually (no previous knowledge required), and learn how to combine them to make interactive web pages. Topics include CSS, the domain object model, HTML forms, sessions, AJAX, jQuery, and the Model-View-Controller pattern.