Student Projects
Bernard Sufrin, November 29, 2025 & January 19, 2026
Programming Language Implementation
PicoML is a polymorphically-typed lazy functional language with I/O actions (cf the I/O Monad in Haskell). It has a very flexible concrete syntax, and a very straightforward polymorphic type system. Its only implementation - a prototype - is written in OCaml as direct, closure-based, abstract-syntax tree interpreter. PicoML GitHub Repository
We would like to see a more efficient implementation, as well as one that would make it straightforward to incorporate new features for engaging with external entities (graphics, etc)
The present project would reimplement the language in one or both of the following ways, each of which would first require a reimplementation of parser and type checker – possibly, but not necessarily, in Scala.
as a closure-based, abstract-syntax tree interpreter using continuations.
as a (Scala) compiler translating to code for an abstract machine - possibly the G-Machine of Lennart Augustsson and Thomas Johnsson - thence to executable code for conventional architecture.
The outcome of the project should be both useable and scrutable: students should be able to read the code of a realistic language implementation.
We think that the PicoML language implementation described above would be a very good basis for a new implementation of a simplified variant of Haskell, suitable for introducing that language in such a way that the need for type classes emerges organically from programming practice.
The project would aim to deliver an implementation suitable for use by Haskell novices that would place emphasis on good error diagnostics: both type errors and runtime errors. Availability of such an implementation could make the teaching of functional programming is the secondary school CS curriculum and for home study a practical proposition: thereby liberating at least some pupils from the conceptual straightjackets of Python, C++, etc.
An important difficulty students have with Haskell and its type system is the (important) notion of type classes: whilst very useful to more advanced Haskell users, they can pose a barrier to learning because what might (in their absence) be a type-error that is straightforward to report and to diagnose, gets reported in terms of instances and classes. For example:
ghci> max xs
<interactive>:2:1: error:
• No instance for (Show ([Integer] -> [Integer]))
arising from a use of ‘print’
(maybe you haven't applied a function to enough arguments?)
• In a stmt of an interactive GHCi command: print it
ghci> max
<interactive>:1:1: error:
• No instance for (Show (() -> () -> ()))
arising from a use of ‘print’
(maybe you haven't applied a function to enough arguments?)
• In a stmt of an interactive GHCi command: print itOf course wise neophytes take their tutors’ advice, and explore the type of the function they thought they were using correctly:
ghci> :t max
max :: Ord a => a -> a -> aand may then realize that what they were after is
ghci> :t maximum
maximum :: (Foldable t, Ord a) => t a -> aBut what’s a Foldable? The neophyte has to understand that it’s a constructor class! And the most succinct explanation of that that can be found is
“A constructor class is declared with a type parameter of kind
* -> *, * -> * -> *In other words: a constructor class describes behaviour of type constructors, not of ground types.”
Thus in order to understand an inscrutable diagnosis of simple mistake made in writing in a simple language, our neophyte must take on board explanations of advanced ideas (type class, kind, etc) that can only be understood once the simpler language has been mastered.
Proof Support for a Haskell-like language
The purpose of this project would be to implement an interactive system to support the discovery (and pretty presentation) of equational proofs by a combination of “automatic choice” and human guidance. Richard Bird, acknowledging Mike Spivey’s unpublished work, sketched an implementation of the simplest form of such a “proof assistant” in Haskell in his most excellent book: Thinking Functionally with Haskell. The project would start by implementing a similar assistant with a convenient interactive workflow for discovering, recording, and checking proofs.
The tool should also support the use of appropriate induction rules derived automatically from data declarations.
An interesting challenge will be the provision of convenient methods for providing human guidance for the application of algebraic laws (such as associativity, commutativity, distributivity) at appropriate points in a proof. Although now somewhat long in the tooth, the Jape generic proof editor still provides (in its functional programming example theory) a working concrete example of the sort of guidance that could be used here, and a user interface by which such guidance can be communicated. Our slogan while building Jape (and many of its example theories) was “Proof by Pointing”. The Jape GitHub repository is here.
Many Haskell proofs take the form of straightforward equational rewriting using definitions or derived laws left-to-right as rules. Typically the discovery of a proof of
lhs = rhswill take the form
lhs
= { rule name
lhs1
= { rule name
lhs2
.
lhsn
= { rule name}
crux followed by
rhs
= { rule name
rhs1
= { rule name
rhs2
...
rhsm
= { rule name
cruxWhere crux is the common term to which both sides can be reduced. This style of presentation relies implicitly on the transitivity of equality.
Aside: it is annoying that some authors obfuscate these sensible discovery steps by a linearised presentation “as if” the post-crux proof had been discovered by using rules ``right to left’’
...
crux
= { rule name
rhsm
= { rule name
...
rhs2
= { rule name
rhs1
= { rule name
rhsIn our experience such presentations can be pedagogically harmful.
Sometimes the choice of rule at each stage is almost automatic: “pretend you are the Haskell interpreter”. At other times firm human guidance (and/or the invention of lemmas) is needed. For example, a proof of
(rev * rev) . swap . (rev * rev) . swap
=
...
=
idin the presence of laws/definitions
rev . rev = id
swap(y,z) = (z,y)
(f * g)(y, z) = (f x, g y)can use the lemmas
swap . (f*g) . swap = g*f
(f * g) . (h *j) = (f . h) * (g . j)as well as timely invocation of the associativity of composition.
Proof by Pointing: Lean meets Jape
What?
For many years the generic proof-editor Jape has been providing a "proof by pointing" graphical user interface to support the human-directed discovery of proofs and derivations in a logic defined as a system of inference rules. The goal of this project is not to reinvent Jape, but to give it a modern semantic substrate, using Lean4: the most recent implementation of a very widely accepted programming language cum proof assistant (See https://lean-lang.org/).
The first substantive piece of work will be come up with a proof of concept implementation of proof-by-pointing in the Jape style for one, perhaps two, straightforward logics. I favour (but don't wish to be dogmatic about) a single-conclusion-sequent presentation of a first-order logic, for example, the logic used in Introduction to Formal Proof. I also favour (but don't wish to be dogmatic about) using Scala as the language in which to program the front-end.1
Why?
Jape was ahead of its time in several respects:
Proof by pointing rather than scripting
Explicit proof-derivation objects evolving (interactive) step-by-step
Structural views of proof derivations: Fitch-boxed or as inference trees: not just as linear text
A focus on pedagogy through human interaction, not just the correctness of derivations.
At the time Richard Bornat and I designed it Jape was revolutionary in the way it provided straightforward user-directed construction of proofs, as well as supporting a straightforward "logician oriented" metalanguage for defining inference systems. There are few constraints on the kinds of "logic" with which Jape can cope: our goal was always to make it possible for someone who isn’t expert in Jape to construct a Jape inference system capable of capturing their logic, proof system, operational semantics, or what-have-you more or less directly from its presentation in a textbook or paper; then for others to construct derivations in the system interactively.
Our motivation, and the principles behind Jape's end-user interfaces, were eventually articulated in a couple of papers delivered at the "User Interfaces for Theorem Provers" conference series that it had catalysed: User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures, and User Interfaces for Generic Proof Assistants Part II: Displaying Proofs and in the (shorter) Formal Aspects of Computing Paper: A Minimal Graphical User Interface for the Jape Proof Calculator. These and others that may be of interest are still readable in the directory https://www.cs.ox.ac.uk/people/bernard.sufrin/jape.org.uk/DOCUMENTS/CURRENT/.
When Jape was born, and for very many years afterwards, nearly all of the work in user interfaces for proof tools addressed the problem(s) of attaching a user interface to a powerful pre-existing proof assistant/theorem prover. Our experience of teaching people to conduct proofs (and other derivations) led us to reject this approach.
Jape’s semantic substrate was defined by a carefully constructed inference engine; but at the time of its design we were uninterested in foundational aspects of that engine. The advent of Lean4 has given fresh impetus to the idea of re-embodying the UI principles of Jape in a new logical setting.
Note
Subsequent projects ought to be able to take this proof of concept in the direction of other logics (Modal logics, Program logics, Separation logic, etc) and systems formalisable as inference systems. The research challenges there include finding straightforward ways for the "interaction designer" to describe correspondences between user-gestures and the inference rules / tactics to which they should be bound.2
Embedded Handel for Hardware Design
HANDEL (designed in this Department by the hardware compilation group led by Ian Page) was one of the very earliest serious attempts to demonstrate that
Hardware should be described by a programming language, not as wires and registers.
The key ideas of Handel were rooted in: strong static typing, concurrency as a first-class concept, and its semantics were rooted in csp / occam. For comparison with a somewhat lower-level language in which concurrency is implicit, see [4].
In its prototype implementation it was embedded (in a niche-programming language: Standard ML). Its successful application to designs that were to be implemented using (then nascent) Field Programmable Gate Array technology[1,2] led to a successor language, Handel-C[3], being built commercially, and adopted as a hardware design tool of choice within the academic community, especially in the United Kingdom. The demise of Handel-C has been authoritatively attributed to the very high cost and proprietary nature of parts of its toolchain.
These days FPGAs are available at a variety of scales, for example (high end) AMD/Xilinx "Virtex" Ultrascale with ~9 million logic cells, costing tens of thousands of pounds per chip and (low end) Lattice CE40UP5K with up to ~5,000 cells with typical board costs of a few tens of pounds. Lattice is well supported by open toolchains. The time is ripe for reviving Handel.
The goal of this project is to embed an implementation of Handel in Scala, generating output for synthesis by an open-source tool-chain.
References:
https://www.cs.ox.ac.uk/people/bernard.sufrin/personal/HANDEL/pproc.pdf - PARAMETRISED PROCESSOR GENERATION
https://www.cs.ox.ac.uk/people/bernard.sufrin/personal/HANDEL/wotug94v - Automatic Design and Implementation of Microprocessors
https://en.wikipedia.org/wiki/Handel-C - HANDEL-C
I developed the Glyph User Interface Toolkit (github.com/sufrin/Glyph) for purposes such as this.↩︎
The Jape tactic language had binding constructs to facilitate this; but its rebarbative syntax and ad-hoc semantics meant that Bornat and Sufrin were almost the only people who could use it.↩︎