A new generation of textual corpora: mining corpora from very large collections. - Gordon Stewart 001; Gregory R. Crane; Alison Babeu (JCDL, 2007)

Local actions for a curry-style operational semantics. - Gordon Stewart 001; Andrew W. Appel (PLPV, 2011)

Verified heap theorem prover by paramodulation. - Gordon Stewart 001; Lennart Beringer; Andrew W. Appel (ICFP, 2012)

Computational Verification of Network Programs in Coq. - Gordon Stewart 001 (CPP, 2013)

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. - Gordon Stewart 001; Anindya Banerjee 001; Aleksandar Nanevski (PPDP, 2013)

Portable Software Fault Isolation. - Joshua A. Kroll; Gordon Stewart 001; Andrew W. Appel (CSF, 2014)

Verified Compilation for Shared-Memory C. - Lennart Beringer; Gordon Stewart 001; Robert Dockins; Andrew W. Appel (ESOP, 2014)

Poster: Ziria: language for rapid prototyping of wireless PHY. - Mahanth Gowda; Gordon Stewart 001; Geoffrey Mainland; Bozidar Radunovic; Dimitrios Vytiniotis; Doug Patterson (MobiCom, 2014)

Demo: 802.11 a/g PHY implementation in ziria, domain-specific language for wireless programming. - Gordon Stewart 001; Mahanth Gowda; Geoffrey Mainland; Bozidar Radunovic; Dimitrios Vytiniotis (SRIF@SIGCOMM, 2014)

Ziria: language for rapid prototyping of wireless PHY. - Gordon Stewart 001; Mahanth Gowda; Geoffrey Mainland; Bozidar Radunovic; Dimitrios Vytiniotis; Doug Patterson (SIGCOMM, 2014)

Ziria: A DSL for Wireless Systems Programming. - Gordon Stewart 001; Mahanth Gowda; Geoffrey Mainland; Bozidar Radunovic; Dimitrios Vytiniotis; Cristina Luengo Agullo (ASPLOS, 2015)

Demo: Implementation of Real-time WiFi Receiver in Ziria, Language for Rapid Prototyping of Wireless PHY. - Gordon Stewart 001; Mahanth Gowda; Geoffrey Mainland; Bozidar Radunovic; Dimitrios Vytiniotis (MobiCom, 2015)

Compositional CompCert. - Gordon Stewart 001; Lennart Beringer; Santiago Cuéllar; Andrew W. Appel (POPL, 2015)

Verified Separate Compilation for C - Gordon Stewart 001 (2015)

Verified perceptron convergence theorem. - Charlie Murphy; Patrick Gray; Gordon Stewart 001 (MAPL@PLDI, 2017)

Brief Announcement: Certified Multiplicative Weights Update: Verified Learning Without Regret. - Alexander Bagnall; Samuel Merten; Gordon Stewart 001 (PODC, 2017)

Training Ensembles to Detect Adversarial Examples. - Alexander Bagnall; Razvan C. Bunescu; Gordon Stewart 001 (CoRR, 2017)

A Library for Algorithmic Game Theory in Ssreflect/Coq. - Alexander Bagnall; Samuel Merten; Gordon Stewart 001 (J. Formaliz. Reason., 2017)

Verified Learning Without Regret - From Algorithmic Game Theory to Distributed Systems with Mechanized Complexity Guarantees. - Samuel Merten; Alexander Bagnall; Gordon Stewart 001 (ESOP, 2018)

Snårkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell. - Gordon Stewart 001; Samuel Merten; Logan Leland (PADL, 2018)

GARUDA: Designing Energy-Efficient Hardware Monitors From High-Level Policies for Secure Information Flow. - Seaghan Sefton; Taiman Siddiqui; Nathaniel St. Amour; Gordon Stewart 001; Avinash Karanth Kodi (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2018)

Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. - Alexander Bagnall; Gordon Stewart 001 (AAAI, 2019)

Developing With Formal Methods at BedRock Systems, Inc. - Gregory Malecha; Gordon Stewart 001; Frantisek Farka; Jasper Haag; Yoichi Hirai (IEEE Secur. Priv., 2022)

DAGGER: Exploiting Language Semantics for Program Security in Embedded Systems. - Garret Cunningham; Harsha Chenji; David Juedes; Gordon Stewart 001; Avinash Karanth (ISQED, 2023)

Inductive Reasoning for Coinductive Types. - Alexander Bagnall; Gordon Stewart 001; Anindya Banerjee 001 (CoRR, 2023)

Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning. - Alexander Bagnall; Gordon Stewart 001; Anindya Banerjee 001 (Proc. ACM Program. Lang., 2023)