Steven Obua

Publication Activity (10 Years)

Years Active: 2005-2023
Publications (10 Years): 11

Top Venues

CoRR

MKM/Calculemus/DML

ICTAC

CICM

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Steven Obua
Logic is Algebra. CoRR (2023)
Steven Obua
Abstraction Logic: A New Foundation for (Computer) Mathematics. CoRR (2022)
Steven Obua
Local Lexing. Arch. Formal Proofs 2017 (2017)
Phil Scott, Steven Obua, Jacques D. Fleuriot
Bootstrapping LCF Declarative Proofs. CoRR (2017)
Steven Obua
Parameterized Local Lexing. CoRR (2017)
Steven Obua, Phil Scott, Jacques D. Fleuriot
Local Lexing. CoRR (2017)
Phil Scott, Steven Obua, Jacques D. Fleuriot
Compiling Purely Functional Structured Programs. CoRR (2017)
Jacques D. Fleuriot, Steven Obua, Phil Scott
Social Network Processes in the Isabelle and Coq Theorem Proving Communities. CoRR (2016)
Steven Obua, Phil Scott, Jacques D. Fleuriot
ProofScript: Proof Scripting for the Masses. ICTAC (2016)
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
Type Inference for ZFH. CICM (2015)
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
A formal proof of the Kepler conjecture. CoRR (2015)
Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall
ProofPeer: Collaborative Theorem Proving. CoRR (2014)
Steven Obua, Mark Adams, David Aspinall
Capturing Hiproofs in HOL Light. CoRR (2013)
Steven Obua, Mark Adams, David Aspinall
Capturing Hiproofs in HOL Light. MKM/Calculemus/DML (2013)
Steven Obua
ProofPeer - A Cloud-based Interactive Theorem Proving System CoRR (2012)
Steven Obua
Purely Functional Structured Programming CoRR (2010)
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. 44 (1) (2010)
Steven Obua
Syntax and Semantics of Babel-17 CoRR (2010)
Steven Obua, Tobias Nipkow
Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell. 56 (3-4) (2009)
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
Invariants, Modularity, and Rights. Ershov Memorial Conference (2009)
Steven Obua
Proof Pearl: Looping Around the Orbit. TPHOLs (2007)
Steven Obua, Sebastian Skalberg
Importing HOL into Isabelle/HOL. IJCAR (2006)
Steven Obua
Checking Conservativity of Overloaded Definitions in Higher-Order Logic. RTA (2006)
Steven Obua
Partizan Games in Isabelle/HOLZF. ICTAC (2006)
Steven Obua
Proving Bounds for Real Linear Programs in Isabelle/HOL. TPHOLs (2005)
Steven Obua
Proving Bounds for Real Linear Programs in Isabelle/HOL. Mathematics, Algorithms, Proofs (2005)

Steven Obua.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Steven Obua