Thesis

I have submitted my PhD thesis, and am awaiting a viva. This page includes a draft copy of my thesis, along with some of the documents from earlier stages. The thesis comprises of 4 main content chapters, based on the following pieces of work:

• Uniplate - generic programming.
• Supero - supercompilation and program optimisation.
• Firstify - defunctionalisation.
• Catch - static safety of pattern-matching.

Downloads

• darcs get --partial http://www.cs.york.ac.uk/fp/darcs/ndm/thesis
• Transformation and Analysis of Functional Programs - from my viva presentation (bibtex)(hide bibtex)
  @misc{mitchell:thesis_2008_7_14
      ,title          = "Transformation and Analysis of Functional Programs"
      ,author         = "Neil Mitchell"
      ,year           = "2008"
      ,month          = "July"
      ,day            = "14"
      ,note           = "Presentation from my viva presentation"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-transformation_and_analysis_of_functional_programs-14_jul_2008.pdf'"
  }
  
• Transformation and Analysis of Functional Programs - Initial submission of PhD thesis (abstract)(hide abstract)
  This thesis describes techniques for transforming and analysing functional programs. We operate on a core language, to which Haskell programs can be reduced. We present a range of techniques, all of which have been implemented and evaluated.
  
  We make programs shorter by defining a library which abstracts over common data traversal patterns, removing boilerplate code. This library only supports traversals having value-specific behaviour for one type, allowing a simpler programming model. Our library allows concise expression of traversals with competitive performance.
  
  We make programs faster by applying a variant of supercompilation. As a result of practical experiments, we have identified modifications to the standard supercompilation techniques -- particularly with respect to let bindings and the generalisation technique.
  
  We make programs safer by automatically checking for potential pattern-match errors. We define a transformation that takes a higher-order program and produces an equivalent program with fewer functional values, typically a first-order program. We then define an analysis on a first-order language which checks statically that, despite the possible use of partial (or non-exhaustive) pattern matching, no pattern-match failure can occur.
  (bibtex)(hide bibtex)
  @unpublished{mitchell:thesis_2008_6_4
      ,title          = "Transformation and Analysis of Functional Programs"
      ,author         = "Neil Mitchell"
      ,year           = "2008"
      ,month          = "June"
      ,day            = "4"
      ,note           = "Draft, Initial submission of PhD thesis"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/draft-transformation_and_analysis_of_functional_programs-4_jun_2008.pdf'"
  }
  
• Transformation and Analysis of Haskell Source Code - from my thesis seminar (bibtex)(hide bibtex)
  @misc{mitchell:thesis_2007_7_2
      ,title          = "Transformation and Analysis of {Haskell} Source Code"
      ,author         = "Neil Mitchell"
      ,year           = "2007"
      ,month          = "July"
      ,day            = "2"
      ,note           = "Presentation from my thesis seminar"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-transformation_and_analysis_of_haskell_source_code-02_jul_2007.pdf'"
  }
  
• Catch, Lazy Termination - from PLASMA (bibtex)(hide bibtex)
  @misc{mitchell:thesis_2006_3_16
      ,title          = "Catch, Lazy Termination"
      ,author         = "Neil Mitchell"
      ,year           = "2006"
      ,month          = "March"
      ,day            = "16"
      ,note           = "Presentation from PLASMA"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-catch-16_mar_2006.pdf'"
  }
  
• Qualifying Dissertation: Unfailing Haskell (abstract)(hide abstract)
  Programs written in Haskell may fail at runtime with either a pattern match error, or with non-termination. Both of these can be thought of as giving the value _|_ as a result. Other forms of failure, for example heap exhaustion, are not considered.
  
  The first section of this document reviews previous work, including total functional programming and sized types. Attention is paid to termination checkers for both Prolog and various functional languages.
  
  The main result from work so far is a static checker for pattern match errors that allows non-exhaustive patterns to exist, yet ensures that a pattern match error does not occur. It includes a constraint language that can be used to reason about pattern matches, along with mechanisms to propagate these constraints between program components.
  
  The proposal deals with future work to be done. It gives an approximate timetable for the design and implementation of a static checker for termination and pattern match errors.
  (bibtex)(hide bibtex)
  @misc{mitchell:thesis_2005_6_30
      ,title          = "Qualifying Dissertation: Unfailing {Haskell}"
      ,author         = "Neil Mitchell"
      ,year           = "2005"
      ,month          = "June"
      ,day            = "30"
      ,institution    = "University of York"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/paper-qualifying_dissertation-30_jun_2005.pdf'"
  }
  
• Termination checking for a lazy functional language - from my first year literature review seminar (bibtex)(hide bibtex)
  @misc{mitchell:thesis_2004_12_21
      ,title          = "Termination checking for a lazy functional language"
      ,author         = "Neil Mitchell"
      ,year           = "2004"
      ,month          = "December"
      ,day            = "21"
      ,note           = "Presentation from my first year literature review seminar"
      ,url            = "\verb'http://www-users.cs.york.ac.uk/~ndm/downloads/slides-termination_checking_for_a_lazy_functional_language-21_dec_2004.pdf'"
  }
  

Tags: popular thesis