I primarily teach courses in the areas of programming languages and computer security.

CS 4160: Formal Verification

This course was inaugurated in Spring 2019. An introduction to formal verification, focusing on correctness of functional and imperative programs relative to mathematical specifications. Topics include computer-assisted theorem proving, logic, programming language semantics, and verification of algorithms and data structures. Assignments involve extensive use of a proof assistant to develop and check proofs.

Recent offerings: [Spring 2019]

CS 3110: Data Structures and Functional Programming

This course is the third and final course in the programming sequence for the CS major. It has a long history in the Cornell Computer Science curriculum, evolving from Scheme to SML to OCaml. In my conception of the course, its primary objective is to form students as excellent programmers. The topics in the course title are important but secondary to that objective.

I have evolved the course over the last couple years to strengthen students' programming skills. The twice weekly recitation sections now center on students solving coding exercises with one another and with the assistance of TAs. The programming assignments now usually involve building a cohesive piece of loosely specified software. Students thus get practice with solving small, well specified problems in the recitations, and with creative design and implementation in the out-of-class assignments.

In the first unit of the course when students are learning the basics of functional programming, which is new to most of them, I frame the material as not just learning a new language, but learning how to learn a new language, because that is something they will be doing multiple times throughout their career. We move from informal but careful descriptions of the language syntax and semantics, to a rigorous operational semantics, to a programming assignment in which they implement a substantial fragment of OCaml inside of OCaml itself.

The final project in the course is now open ended: students choose their own requirements, write a design document that is critiqued by TAs, and implement over the course of a month. This process is supported by the integration of some software engineering material into the rest of the course, including architecture, design, testing, and teamwork. In the first trial run of this project, three teams built particularly impressive systems: a sophisticated Pokémon game, an extensible editor in the style of Emacs, and a computer algebra system in the style of Mathematica.

Recent offerings: [Fall 2018] [Fall 2017] [Fall 2016] [Fall 2015] [Spring 2015] [Fall 2014]

CS 5430: System Security

This course is a Master's level introduction to computer security. In my conception of the course, its primary objective is to teach principles for building secure software systems. A principled approach is a quintessential part of the Cornell Computer Science ethos. Students may come from diverse backgrounds but are expected to be familiar with computer systems at the level of a undergraduate senior operating systems course.

The first unit of the course is devoted to teaching students to think clearly about security, with an emphasis on requirements and analysis. Then we cover applied cryptography as a tool: not how to implement or create cryptographic primitives, but how to use them responsibly. The rest of the course is organized around the Gold Standard: audit, authentication and authorization.

Course assignments have included thinking through the security goals for computer systems, learning to program with cryptographic primitives correctly, and solving real-world problems that have no "right" answer such as automated detection of intrusion attempts and password strength estimation.

Historically the course has included a team project in which students built a piece of software and attempted to secure it. To better provide close mentoring of the project, I have now factored it out into a separate practicum. Teams build their software over the course of five deliverables, inspired by a SCRUM-based agile software development process. At each deliverable, the teams receive peer feedback from one another on the security and usability of their software, as well as detailed feedback from me.

Recent offerings: [Spring 2017] [Spring 2016] [Spring 2015]

CS 1380: Data Science For All

This course was inaugurated in Spring 2018. Given data from economics, medicine, biology, or physics, collected from internet denizens, survey respondents, or wireless sensors, how can one understand the phenomenon generating the data, make predictions, and improve decisions? We focus on building skills in inferential thinking and computational thinking, guided by the practical questions we seek to answer. The course teaches critical concepts and skills in computer programming and statistical inference, in conjunction with hands-on analysis of real-world datasets, including economic data, document collections, geographical data, and social networks. We will also consider social issues in data analysis such as privacy and design. Cross-listed with ORIE 1380 and STSCI 1380.

Recent offerings: [Spring 2018]

CS 2110: Object-Oriented Programming and Data Structures

Recent offerings: [Spring 2019]

Summer Schools

I often lecture at summer schools, sometimes lecturing on my own research, and sometimes teaching material from courses that I regularly teach during the academic year.

Teaching History


I am interested in reasoning about software systems and their security. Topics of particular interest include electronic voting, security policies, information flow, cryptography, semantics, logics, language-based security, and specification and verification of programs. A complete list of my publications and talks is available.


Professional Activites