Computer Laboratory

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.


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.