papers
Publications (12)
cs.PL2017
Compiling Purely Functional Structured Programs
Phil Scott, Steven Obua, Jacques Fleuriot
math.MG2009
A revision of the proof of the Kepler conjecture
Thomas C. Hales, John Harrison, Sean McLaughlin +3
cs.MS2012
ProofPeer - A Cloud-based Interactive Theorem Proving System
Steven Obua
math.MG2015
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19
cs.PL2011
Purely Functional Structured Programming
Steven Obua
cs.LO2017
Bootstrapping LCF Declarative Proofs
Phil Scott, Steven Obua, Jacques Fleuriot
cs.LO2017
Local Lexing
Steven Obua, Phil Scott, Jacques Fleuriot
cs.LO2017
Parameterized Local Lexing
Steven Obua
cs.LO2013
Capturing Hiproofs in HOL Light
Steven Obua, Mark Adams, David Aspinall
cs.PL2011
Syntax and Semantics of Babel-17
Steven Obua
cs.SI2016
Social Network Processes in the Isabelle and Coq Theorem Proving Communities
Jacques Fleuriot, Steven Obua, Phil Scott
cs.LO2014
ProofPeer: Collaborative Theorem Proving
Steven Obua, Jacques Fleuriot, Phil Scott +1