Mark Wassell
I am a PhD student supervised by
Prof. Peter Sewell. I am looking at the 'Semantic Tools' task of the
REMS programme with a focus on the
Ott and
Lem tools. I am a member of
Wolfson College. For a more detailed biography see my
LinkedIn profile.
I am chair of
Phoenix Korfball Club and results officer for the
Cambridgeshire Korfball League.
Research Interests
My research is looking at type systems for programming languages and formalising
these in Isabelle with a view to generating an implementation and test oracle
from the formalism.
Supervision
Working Drafts/Submitted
Mechanised Metatheory for the Sail ISA Specification Language.
Mark Wassell, Alasdair Armstrong, Neel Krishnaswami, Peter Sewell, Submitted to CPP 2019.
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, Peter Sewell. Draft, submitted for publication July 2018.
MiniSail - A Core Calculus for Sail Supplementary material for the above detailing MiniSail and the proofs of safety.
Papers/Extended Abstracts
Formalisation of MiniSail in the Isabelle Theorem Prover.
Alasdair Armstrong, Neel Krishnaswami, Peter Sewell and Mark Wassell, Automated Reasoning Workshop, Cambridge, 2018.
Industrial Experience
I have been involved with developing software in the area of
Geographic Information Systems
using a number of languages
(e.g.
Magik)
and platform technologies
(e.g.
Smallworld).
Much of this work has been for customers in the telecommunications sector.
These systems store data about the customers network assests (for example,
cables, cabinets, rack mounted equipment, as well as the services that run across them) and
assist in the operation of the network and planning future changes.
Recently I was developing similar products using a JavaScript, Python, Apache and Postgres stack.
Unpublished Work
Development of Integral Transforms in the Isabelle Interactive Theorem
Prover - MPhil, Computer Laboratory, Cambridge, 2016
Abstract: This dissertation describes a development of the Fourier, Laplace and Mellin
integral transforms within the Isabelle proof assistant and includes example
applications of these transforms. This development extends the complexity of
mathematics encoded in Isabelle and provides a base for further formalisation
of these transforms in Isabelle and verication of algorithms and systems that
make use of the transforms. The development has helped to highlight the
difference between conventional mathematics as done by mathematicians and
mathematics done on a computer. Arising out of the work are also a number
of suggested improvements to Isabelle.
Estimating a Critical Exponent for the Self-Avoiding Walk - Post Graduate Diploma Thesis, University of Melbourne, 2011
Abstract: A self-avoiding walk is a path on a graph with the constraint that no vertex is
visited twice. Typically the graph is in the form of a lattice defined
on points in \(\mathbb{Z}_d\) where \(d\) is the dimension of the lattice. One key
question is how many walks of length \(n\) there are on a particular lattice.
Even though the problem is
simple to state, there is no known exact solution to this question. However,
there is overwhelming evidence that the number of self-avoiding walks of
length \(n\) is asymptotically \(c_n \approx A \mu^n n^{\gamma-1} \)
where \(\mu\) is known as the connective constant and \(\gamma\)
is a critical exponent.
Estimating this critical exponent can be done by counting
the number of walks for lengths up to some maximum and using series analysis
techniques to derive an estimate. On the cubic lattice the current best technique
enumerates only up to \(n = 36\). We have developed a new enumeration algorithm,
which we call dynamic trimerisation, and implemented this on a Graphics
Processing Unit (GPU). The GPU architecture offers a new processing platform
with the benefit of greater performance, however there are a number of challenges
to overcome when implementing on the GPU. The algorithm implemented
compares well to existing enumeration algorithms and with further development
of GPU technology it will be a fruitful direction of research. In conjunction with
the above, we have used dynamic trimerisation for the enumeration of Domb-
Joyce walks. The Domb-Joyce model is a more general model where we allow
the walk to interact with itself but assign a weight, \(w\), to penalise
interacting walks.
Since Domb-Joyce walks with \(w \lt 1\) belong to the same universality
class as self-avoiding walks, we have investigated the use of the Domb-Joyce model to obtain
estimates for the critical exponent.
Semantic Optimisation of Datalog Programs - MSc, University of Cape Town
Abstract: Datalog is the fusion of Prolog and Database technologies aimed at producing
an efficient, logic-based, declarative language for databases.
This fusion takes the best of logic programming for the syntax of Datalog, and the
best of database systems for the operational part of Datalog.
As is the case with all declarative languages, optimisation is necessary to improve
the efficiency of programs. Semantic optimisation uses meta-knowledge describing the data in the database to optimise queries and rules, aiming to reduce the resources
required to answer queries.
In this thesis, I analyse prior work that has been done on semantic optimisation and
then propoe an optimisation system for Datalog that includes optimisation of recursive
programs and and semantic knowledge management module. The language DatalogIC, which is
an extension of Datalog that allows semantic knowledge to be expressed, has also been device
as an implementation vehicle.
Finally empirical results concerning the benefits of semantic optimisation are reported.