Thesis
I am currently completing my PhD thesis. This page includes documents associated with the thesis, and will include the final thesis when available.
Downloads
- darcs get --partial http://www.cs.york.ac.uk/fp/darcs/ndm/thesis
- 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.(bibtex)(hide bibtex)
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.@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'"
}