Publications

Conferences

• Type homogeneity is not a restriction for safe recursion schemes, 2009 To be published. Paper (pdf)

• 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

• The Safe Lambda Calculus BCTCS 2007. Slides (pdf)

• The Safe Lambda Calculus FOCS group lunchtime meeting. Slides (pdf)

Journals

• Evaluating Lambda Terms with Traversals Theoretical Computer Science | September 2019 https://www.sciencedirect.com/science/article/abs/pii/S0304397519305316?via%3Dihub

• The Safe Lambda Calculus With C.-H. Luke Ong. Logical Methods in Computer Science (LMCS), Volume 5, Issue 1, Paper 4. Download (pdf)

• 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)

Theses

• D.Phil. Thesis: The Safe Lambda Calculus 2009, Oxford University Research Archive Download thesis (pdf), Download Erratum (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 =      {https://william.famille-blum.org/},
  year =         {2006},
  month =        {August}
  keywords =     {lambda calculus, game semantics, incrementally justified strategies},
  }
  

• Master's Thesis: Termination analysis of lambda calculus and a subset of core ML 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 = {https://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}
  }