CS565: Programming Languages

Fall 2020 Fall 2018 Fall 2016

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.

CS590: Advanced Topics in Programming Languages

Spring 2020

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.

CS307: Software Engineering

Spring 2019

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.

CS 456: Programming Languages

Spring 2018

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 modularity. Work in the course involves exploring programming languages and features both as a user (by writing programs in those languages), as a language designer (by implementing interpreters for those languages), and as a scholar (by proving mathematical properties of them). We will investigate approaches to modularity such as data abstraction, inheritance, and polymorphism independent of their realization in any particular language. The course will also offer a 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 efficient and correct programs in a functional programming language, Haskell.
  2. Precisely formulate the syntax and runtime behavior of a programming language.
  3. Specify different notions of type safety for a programming language and reason about a programming language's semantics via mathematical induction.
  4. Distinguish between different approaches to modularity and abstraction provided by programming languages.

The course is structured into five sections, the first four of which roughly align with these topics. The final section will consider the realization of some of these ideas in Rust, a modern systems programming language.

CS590: Software Synthesis

Spring 2017

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.

CS105: Computer Programming: PHP/SQL (UT Austin)

Fall 2013 Spring 2013

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.