To return to my main page click here.
I have not produced an exceptional amount of work but all that I produce will appear here (eventually). Anyone downloading these files accepts that there may be mistakes in them for which I do not apologise. Maybe with time I may get round to correcting them but only if I get really bored or enough people pressure me.
Elliptic Functions
My second year essay from Warwick. Elliptic.dvi Elliptic.ps Elliptic.pdf
A Proof of the De Rham Theorem using Open Sets
An investigation of the use of applied lambda-calculi to organise the recursive functionals originally developed by Gödel, Kleene, Grzegorczyk, Platek and others
This thesis contains an analysis of various systems equivalent to Gödel's T, a discussion of various lambda-translation algorithms and an analysis of the systems of Kleene and Platek at the first order level.
Msc.dvi Msc.ps Msc.pdfA Lambda Abstraction Algorithm
We describe and illustrate an algorithm for simulating lambda-abstraction which has been around for many years but seems to have been forgotten. Perhaps because the published version is wrong.
abs.dvi abs.ps abs.pdfLambda Abstraction Algorithms
Here are the slides from a seminar I gave on lambda abstraction algorithms. lamalg.dvi lamalg.ps lamalg.pdf
Six Month Report
Here is my six month report. 6report.dvi 6report.ps 6report.pdf
Twelve Month Report
Here is my 12 month report. Note that it was originally submitted with the current drafts of the following two papers. 12report.pdf
Functorial Kripke-Beth-Joyal models of the lambda Pi-calculus I: type theory and internal logic
This is the first of three papers that I aim to complete to achieve my Ph.D.. At present there is still a bit of work to be done on it and the main points are sketched after the abstract. It is viewed at the author's own risks and any feedback will be gratefully appreciated. This is a development of unfinished notes by Prof. David Pym. The date on the paper is the date it was last updated. Kripke1.pdf
Functorial Kripke-Beth-Joyal models of the lambda Pi-calculus II: the LF logical framework
This is the second of three papers that I aim to complete to achieve my Ph.D.. At present there is still a bit of work to be done on it and the main points are sketched after the abstract. It is viewed at the author's own risks and any feedback will be gratefully appreciated. This is a development of unfinished notes by Prof. David Pym. The date on the paper is the date it was last updated. Kripke2.pdf
Logical Frameworks
I gave a talk at the small workshop on Deep Inference in Paris in December 2006. The slides are linked below. The provide an introduction to logical frameworks as well as sketching my own research. pres.pdf
I gave a talk at the TYPES 2007 Workshop in May 2007. The slides are linked below. TYPES.pdf