CS565: Programming Languages

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.

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.