Steven Obua

According to our database, Steven Obua authored at least 25 papers between 2005 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Logic is Algebra.

Steven Obua

CoRR, 2023

2022

Abstraction Logic: A New Foundation for (Computer) Mathematics.

Steven Obua

CoRR, 2022

2017

Bootstrapping LCF Declarative Proofs.

Phil Scott, Steven Obua, Jacques D. Fleuriot

CoRR, 2017

Compiling Purely Functional Structured Programs.

Phil Scott, Steven Obua, Jacques D. Fleuriot

CoRR, 2017

Local Lexing.

Steven Obua, Phil Scott, Jacques D. Fleuriot

CoRR, 2017

Parameterized Local Lexing.

Steven Obua

CoRR, 2017

Local Lexing.

Steven Obua

Arch. Formal Proofs, 2017

2016

Social Network Processes in the Isabelle and Coq Theorem Proving Communities.

Jacques D. Fleuriot, Steven Obua, Phil Scott

CoRR, 2016

ProofScript: Proof Scripting for the Masses.

Steven Obua, Phil Scott, Jacques D. Fleuriot

Proceedings of the Theoretical Aspects of Computing - ICTAC 2016, 2016

2015

A formal proof of the Kepler conjecture.

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

CoRR, 2015

Type Inference for ZFH.

Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

2014

ProofPeer: Collaborative Theorem Proving.

Steven Obua, Jacques D. Fleuriot, Phil Scott, David Aspinall

CoRR, 2014

2013

Capturing Hiproofs in HOL Light.

Steven Obua, Mark Adams, David Aspinall

Proceedings of the Intelligent Computer Mathematics, 2013

2012

ProofPeer - A Cloud-based Interactive Theorem Proving System

Steven Obua

CoRR, 2012

2010

A Revision of the Proof of the Kepler Conjecture.

Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller

Discret. Comput. Geom., 2010

Syntax and Semantics of Babel-17

Steven Obua

CoRR, 2010

Purely Functional Structured Programming

Steven Obua

CoRR, 2010

2009

Flyspeck II: the basic linear programs.

Steven Obua, Tobias Nipkow

Ann. Math. Artif. Intell., 2009

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, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, Sergey Tverdyshev

Proceedings of the Perspectives of Systems Informatics, 2009

2008

Flyspeck II: the basic linear programs.

Steven Obua

PhD thesis, 2008

2007

Proof Pearl: Looping Around the Orbit.

Steven Obua

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

Checking Conservativity of Overloaded Definitions in Higher-Order Logic.

Steven Obua

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Partizan Games in Isabelle/HOLZF.

Steven Obua

Proceedings of the Theoretical Aspects of Computing, 2006

Importing HOL into Isabelle/HOL.

Steven Obua, Sebastian Skalberg

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

Proving Bounds for Real Linear Programs in Isabelle/HOL.

Steven Obua

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005