I am interested in the theory and application of programming languages, both typed and untyped. This covers several areas of computer science, including the semantics of programming languages, the underlying mathematical structures and methods of formal verification.
Working with Steven Ramsay and Robin Neatherway, I was one of the developers of THORS, a type-based model-checker for verifying Alternation-Free Mu Calculus properties (and hence CTL properties) on value trees generated by Higher Order Recursion Schemes. This was the first model-checker for infinite state systems. The intended application of this work was verifying liveness properties of higher order functional programs.
More recently, I have been looking at intensional metaprogramming, in particular the SF-calculus: how to analyse it and how it relates to other forms of metaprogramming.
I am currently developing tools for using the new language Coco to model and verify embedded software.
My undergraduate degree was a BA in Computer Science, gained while studying at Gonville & Caius College, Cambridge (2003-2006). After a period working as a software developer for Autonomy Systems, I studied for the MSc in Mathematics and Foundations of Computer Science at St Edmund Hall College, Oxford (2008-2009). I completed my DPhil in Computer Science at Merton College, Oxford (2009-2015), under the supervision of Luke Ong.
After that, I taught in the department (2013-2017) as a Senior Teaching Assistant and in Balliol College (2014-2017) as their Lecturer in Computer Science.
I was part of the team from Luke Ong's research group that won the ICFP Programming Contest in 2011. Our winning entry was written in the functional programming language F#. In 2014, I was part of the organising committee for the contest, which challenged participants to write AIs for a Pacman clone.
I am currently working as a postdoctoral researcher on a project investigating model-checking of embedded software in control systems, under Bill Roscoe and Philippa Hopcroft.
Information flow analysis for a dynamically typed language with staged metaprogramming
Martin Mariusz Lester‚ Luke Ong and Max Schäfer
In Journal of Computer Security. Vol. 24. No. 5. Pages 541–582. 2016.
Control Flow Analysis for SF Combinator Calculus
In Alexei Lisitsa‚ Andrei P. Nemytykh and Alberto Pettorossi, editors, Proceedings of the Third International Workshop on Verification and Program Transformation‚ VPT@ETAPS 2015‚ London‚ United Kingdom‚ 11th April 2015.. Vol. 199 of EPTCS. Pages 51–67. 2015.
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming
Martin Lester‚ C.−H. Luke Ong and Max Schäfer
In CoRR. Vol. abs/1302.3178. 2013.