Proving Bounds for Real Linear Programs in Isabelle/HOL. - Steven Obua (Mathematics, Algorithms, Proofs, 2005)

Importing HOL into Isabelle/HOL. - Steven Obua; Sebastian Skalberg (IJCAR, 2006)

Partizan Games in Isabelle/HOLZF. - Steven Obua (ICTAC, 2006)

Checking Conservativity of Overloaded Definitions in Higher-Order Logic. - Steven Obua (RTA, 2006)

Proof Pearl: Looping Around the Orbit. - Steven Obua (TPHOLs, 2007)

Flyspeck II: the basic linear programs. - Steven Obua (2008)

Invariants, Modularity, and Rights. - Ernie Cohen; Eyad Alkassar; Vladimir Boyarinov; Markus Dahlweid; Ulan Degenbaev; Mark A. Hillebrand; Bruno Langenstein; Dirk Leinenbach; Michal Moskal; Steven Obua; Wolfgang J. Paul; Hristo Pentchev; et al. (Ershov Memorial Conference, 2009)

Flyspeck II: the basic linear programs. - Steven Obua; Tobias Nipkow (Ann. Math. Artif. Intell., 2009)

Purely Functional Structured Programming - Steven Obua (CoRR, 2010)

Syntax and Semantics of Babel-17 - Steven Obua (CoRR, 2010)

A Revision of the Proof of the Kepler Conjecture. - Thomas C. Hales; John Harrison 001; Sean McLaughlin; Tobias Nipkow; Steven Obua; Roland Zumkeller (Discret. Comput. Geom., 2010)

ProofPeer - A Cloud-based Interactive Theorem Proving System - Steven Obua (CoRR, 2012)

Capturing Hiproofs in HOL Light. - Steven Obua; Mark Adams; David Aspinall 001 (MKM/Calculemus/DML, 2013)

ProofPeer: Collaborative Theorem Proving. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CoRR, 2014)

Type Inference for ZFH. - Steven Obua; Jacques D. Fleuriot; Phil Scott; David Aspinall 001 (CICM, 2015)

A formal proof of the Kepler conjecture. - Thomas C. Hales; Mark Adams; Gertrud Bauer; Dat Tat Dang; John Harrison 001; Truong Le Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Thang Tat Nguyen; Truong Quang Nguyen; Tobias Nipkow; et al. (CoRR, 2015)

ProofScript: Proof Scripting for the Masses. - Steven Obua; Phil Scott; Jacques D. Fleuriot (ICTAC, 2016)

Social Network Processes in the Isabelle and Coq Theorem Proving Communities. - Jacques D. Fleuriot; Steven Obua; Phil Scott (CoRR, 2016)

Local Lexing. - Steven Obua (Arch. Formal Proofs, 2017)

Parameterized Local Lexing. - Steven Obua (CoRR, 2017)

Local Lexing. - Steven Obua; Phil Scott; Jacques D. Fleuriot (CoRR, 2017)

Compiling Purely Functional Structured Programs. - Phil Scott; Steven Obua; Jacques D. Fleuriot (CoRR, 2017)

Bootstrapping LCF Declarative Proofs. - Phil Scott; Steven Obua; Jacques D. Fleuriot (CoRR, 2017)

Abstraction Logic: A New Foundation for (Computer) Mathematics. - Steven Obua (CoRR, 2022)

Logic is Algebra. - Steven Obua (CoRR, 2023)