18 citations · 22 across the 12 of their papers we have counts for
14 papers
Logic is Algebra
Steven Obua
Logic really is just algebra, given one uses the right kind of algebra, and the right kind of logic. The right kind of algebra is abstraction algebra, and the right kind of logic i…
Abstraction Logic: A New Foundation for (Computer) Mathematics
Steven Obua
Abstraction logic is a new logic, serving as a foundation of mathematics. It combines features of both predicate logic and higher-order logic: abstraction logic can be viewed both…
Parameterized Local Lexing
Steven Obua
Building on the concept of local lexing the concept of parameterized local lexing is introduced.
Compiling Purely Functional Structured Programs
Phil Scott, Steven Obua, Jacques Fleuriot
We present a marriage of functional and structured imperative programming that embeds in pure lambda calculus. We describe how we implement the core of this language in a monadic D…
Bootstrapping LCF Declarative Proofs
Phil Scott, Steven Obua, Jacques Fleuriot
Suppose we have been sold on the idea that formalised proofs in an LCF system should resemble their written counterparts, and so consist of formulas that only provide signposts for…
Local Lexing
Steven Obua, Phil Scott, Jacques Fleuriot
We introduce a novel parsing concept called local lexing. It integrates the classically separated stages of lexing and parsing by allowing lexing to be dependent upon the parsing p…
Social Network Processes in the Isabelle and Coq Theorem Proving Communities
Jacques Fleuriot, Steven Obua, Phil Scott
We identify the main actors in the Isabelle and Coq communities and describe how they affect and influence their peers. This work explores selected foundations of social networking…
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the…
ProofPeer: Collaborative Theorem Proving
Steven Obua, Jacques Fleuriot, Phil Scott +1
We define the concept of collaborative theorem proving and outline our plan to make it a reality. We believe that a successful implementation of collaborative theorem proving is a…
Capturing Hiproofs in HOL Light
Steven Obua, Mark Adams, David Aspinall
Hierarchical proof trees (hiproofs for short) add structure to ordinary proof trees, by allowing portions of trees to be hierarchically nested. The additional structure can be used…
ProofPeer - A Cloud-based Interactive Theorem Proving System
Steven Obua
ProofPeer strives to be a system for cloud-based interactive theorem proving. After illustrating why such a system is needed, the paper presents some of the design challenges that…
Syntax and Semantics of Babel-17
Steven Obua
We present Babel-17, the first programming language for purely functional structured programming (PFSP). Earlier work illustrated PFSP in the framework of a toy research language.…
Purely Functional Structured Programming
Steven Obua
The idea of functional programming has played a big role in shaping today's landscape of mainstream programming languages. Another concept that dominates the current programming st…
A revision of the proof of the Kepler conjecture
Thomas C. Hales, John Harrison, Sean McLaughlin +3
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original…