Gordon Stewart

I'm an Assistant Professor in the School of Electrical Engineering and Computer Science at Ohio University.

I do research in programming languages, interactive theorem proving, and software security. I received my PhD in Computer Science from Princeton in 2015 (adviser: Andrew Appel), and an AB from Harvard in 2006. Much of my research software is open source on Github. My picture is here. My CV is here.

Contact Information

Office: 355 Stocker Center
Email: gstewart@ohio.edu
Phone: (740) 593-1578
OH: W2-2:55pm, F10:50-11:45am

News

11/18
Certifying the True Error accepted for publication at AAAI'19
07/18
Serving on the PC for CoqPL 2019, co-located with POPL'19 in Lisbon
06/18
New webpage on verified ML at MLCert.org
12/17
Verified Learning Without Regret accepted to ESOP'18
10/17
Snaarkl, on verifiable computing in Haskell, accepted to PADL'18
05/17
Brief announcement Certified Multiplicative Weights Update accepted to PODC'17
05/17
Verified Perceptron Convergence Theorem accepted to MAPL'17
Older News
03/17
NSF CRII award to support the Cage Project: using algorithmic game theory to build distributed systems with verified complexity by design
10/16
Invited seminar at UToledo EECS: Verified Learning Without Regret: A Mechanized Proof of the Multiplicative Weights Update Algorithm
10/16
New draft paper: Certified Convergent Perceptron Learning together with students Charlie Murphy (ugrad, Princeton grad) and Patrick Gray (grad)
09/16
Funded collaborative research grant on "Intelligent Channel Sensing"
04/16
New website: Programming Languages and Systems at OU
10/15
I'm serving on the PLDI'16 External Review Committee.

Selected Recent Research Papers

See here for a more complete list, or find me on Google Scholar or DBLP. MLCert.org has code links for the most recent papers below.
AAAI'19 Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. Alexander Bagnall and Gordon Stewart. Capsule summary: Machine learning in Coq with verified generalization guarantees, applied via TensorFlow to the extended MNIST Digits dataset
ESOP'18 Verified Learning Without Regret: From Algorithmic Game Theory to Distributed Systems With Mechanized Complexity Guarantees. Samuel Merten, Alexander Bagnall, and Gordon Stewart. Capsule summary: Verified Multiplicative Weights Update in Coq, with applications to online learning and distributed routing
PODC'17 Brief Announcement: Certified Multiplicative Weights Update. Alexander Bagnall, Samuel Merten, and Gordon Stewart.
ASPLOS'15 Ziria: A DSL for Wireless Systems Programming. G. Stewart, M. Gowda, G. Mainland, B. Radunovic, D. Vytiniotis, and C. Luengo Agullo.
POPL'15 Compositional CompCert. Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel.

Students

I'm fortunate to do research with a number of great students at OU, including:

Sponsored Research Projects

Courses

F2019
CS 6930: Independent Study on Verified Systems
F2019
CS 3200: Programming Languages
F2019
CS 4201: Software Verification
S2019
CS 4100: Formal Languages and Compilers
F2018
CS 3200: Programming Languages
F2018
CS 4201: Software Verification
S2018
CS 6900: Advanced Topics in Programming Languages
S2018
CS 4100: Formal Languages and Compilers
F2017
CS 3200: Programming Languages
F2017
CS 4201: Software Verification
S2017
CS 4100: Intro. to Formal Languages and Compilers
F2016
CS 4900/5900: Software Verification
S2016
CS 4100: Intro. to Formal Languages and Compilers
F2015
CS 4900/5900: Software Verification

Talks

The documents contained in these pages are included to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.