Publications

Conference papers and talks

• The Safe Lambda Calculus (extended version)

  With C.-H. Luke Ong.

  Technical report. Long version of the TLCA07 paper.

  Download paper (pdf) | Download slides (pdf)

• The Safe Lambda Calculus

  With C.-H. Luke Ong.

  In Lecture Notes in Computer Science Vol. 4583 of Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications (TLCA07), pages 39-53. © Springer-Verlag Berlin / Heidelberg, 2007.

  Download (pdf) | Bibtex

  @INPROCEEDINGS{blumong:safelambdacalculus,
    author = {William Blum and C.-H. Luke Ong},
    title = {The Safe Lambda Calculus},
    booktitle = {TLCA},
    year = {2007},
    pages = {39-53},
    bibsource = {DBLP, http://dblp.uni-trier.de},
    crossref = {DBLP:conf/tlca/2007},
    ee = {http://dx.doi.org/10.1007/978-3-540-73228-0_5}
  }
  

• A concrete presentation of Game Semantics

  Talk given at Galop workshop (ETAPS 2008)

  Slides (pdf)

• A concrete presentation of Game Semantics

  Talk given at BCTCS 2008

  Slides (pdf)

• Termination analysis of lambda calculus and a subset of core ML

  Talk given at BCTCS 2005

Journal papers

• The Safe Lambda Calculus (submited)

  With C.-H. Luke Ong.

  Submited to Logical Methods in Computer Science (LMCS).

• Local computation of beta-reduction--A concrete presentation of Game Semantics (in preparation)

  With C.-H. Luke Ong.

  Annals of Pure and Applied Logic (APAL), (in preparation).

  Download (pdf)

Thesis

• The Safe Lambda Calculus

  D.Phil. thesis, submitted, Oxford University.

  Download (pdf)

Work, presentations

• The Safe Lambda Calculus

  FOCS group lunchtime meeting.

  Slides (pdf)

• The Safe Lambda Calculus

  BCTCS 2007.

  Slides (pdf)

• DPhil transfer thesis: The Safe Lambda Calculus

  Technical report, submitted August 2006.

  Slides (pdf) | Bibtex

  @MISC{blum-dphiltransfer,
        author =       {William Blum},
        title =        {The safe lambda calculus},
        howpublished = {DPhil transfer thesis, University of Oxford},
        address =      {http://william.famille-blum.org/},
        year =         {2006},
        month =        {August}
        keywords =     {lambda calculus, game semantics, incrementally justified strategies},
  }
  

• Termination analysis of lambda calculus and a subset of core ML

  Master's Thesis. 2004.

  Download (pdf) | Sources (Objective Caml) | Bibtex

  @MASTERSTHESIS{blum-mscthesis,
    AUTHOR = {William Blum},
    TITLE = {Termination analysis of lambda calculus and a subset of core ML},
    SCHOOL = {University of Oxford},
    YEAR = {2004},
    address = {http://william.famille-blum.org/},
    month = {september},
    abstract = {Lee, Jones and Ben-Amram introduced size-change termination,
      a decidable property strictly stronger than termination. They invented 
      a method called the Size-change Principle to analyze it. Based on the 
      work of Jones and Bohr, we propose an extension of the size-change principle 
      to a subset of ML featuring ground type values, higher-order type values and 
      recursively defined functions. This is the first time that the size-change 
      principle is applied to a higher-order functional language. The language 
      handles natively if-then-else and let rec structures. The resulting algorithm 
      produces the expected result for higher-order values but can also analyze 
      the size of ground type values. This enhances the scope of the termination 
      analyzer to some recursively defined function operating on numbers.},
    keywords = {size-change termination, lambda calculus, core ml}
  }
  

This is a disturbance, if you are reading this then you have just been disturbed.