1 citations · 1 across the 4 of their papers we have counts for
4 papers
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…
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…