Steven Obua

27 papers A 1C 3Journal 16Unranked 6
YearRankTypeTitle / Venue / Authors
2023 J jnl
Logic is Algebra.
CoRR
Steven Obua
2022 J jnl
Abstraction Logic: A New Foundation for (Computer) Mathematics.
CoRR
Steven Obua
2017 J jnl
Bootstrapping LCF Declarative Proofs.
CoRR
Phil Scott, Steven Obua, Jacques D. Fleuriot
2017 J jnl
Compiling Purely Functional Structured Programs.
CoRR
Phil Scott, Steven Obua, Jacques D. Fleuriot
2017 J jnl
Local Lexing.
Arch. Formal Proofs
Steven Obua
2017 J jnl
Local Lexing.
CoRR
Steven Obua, Phil Scott, Jacques D. Fleuriot
2017 J jnl
Parameterized Local Lexing.
CoRR
Steven Obua
2016 C conf
ProofScript: Proof Scripting for the Masses.
ICTAC
Steven Obua, Phil Scott, Jacques D. Fleuriot
2016 J jnl
Social Network Processes in the Isabelle and Coq Theorem Proving Communities.
CoRR
Jacques D. Fleuriot, Steven Obua, Phil Scott
2015 J jnl
A formal proof of the Kepler conjecture.
CoRR
Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
2015 C conf
Type Inference for ZFH.
CICM
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
2014 J jnl
ProofPeer: Collaborative Theorem Proving.
CoRR
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
2013 — conf
Capturing Hiproofs in HOL Light.
MKM/Calculemus/DML
Steven Obua, Mark Adams, David Aspinall
2013 J jnl
Capturing Hiproofs in HOL Light.
CoRR
Steven Obua, Mark Adams, David Aspinall
2012 J jnl
ProofPeer - A Cloud-based Interactive Theorem Proving System
CoRR
Steven Obua
2010 J jnl
A Revision of the Proof of the Kepler Conjecture.
Discret. Comput. Geom.
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
2010 J jnl
Purely Functional Structured Programming
CoRR
Steven Obua
2010 J jnl
Syntax and Semantics of Babel-17
CoRR
Steven Obua
2009 J jnl
Flyspeck II: the basic linear programs.
Ann. Math. Artif. Intell.
Steven Obua, Tobias Nipkow
2009 — conf
Invariants, Modularity, and Rights.
Ershov Memorial Conference
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, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev
2008 — —
Flyspeck II: the basic linear programs.
Steven Obua
2007 — conf
Proof Pearl: Looping Around the Orbit.
TPHOLs
Steven Obua
2006 — conf
Checking Conservativity of Overloaded Definitions in Higher-Order Logic.
RTA
Steven Obua
2006 A conf
Importing HOL into Isabelle/HOL.
IJCAR
Steven Obua, Sebastian Skalberg
2006 C conf
Partizan Games in Isabelle/HOLZF.
ICTAC
Steven Obua
2005 — conf
Proving Bounds for Real Linear Programs in Isabelle/HOL.
Mathematics, Algorithms, Proofs
Steven Obua
2005 — conf
Proving Bounds for Real Linear Programs in Isabelle/HOL.
TPHOLs
Steven Obua