Academic Pages of Mark Price

Academic Papers

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

  • This my final year project submitted for my Master of Mathematics degree from the University of Warwick.
  • Abstract
  • An exposition of singular cohomology theory and De Rham chomology leading up to the proof of the De Rham theorem using induction on open sets.
  • DeRham.dvi DeRham.ps DeRham.pdf

    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 is my MSc dissertation.
  • Abstract
  • 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.pdf

    A Lambda Abstraction Algorithm

  • This is a short note produced jointly with H. Simmons.
  • Abstract
  • 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.pdf

    Lambda 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

    To return to my main page click here.