Congratulations to Adam Barwell, who successfully defended his thesis yesterday. Adam’s thesis was supervised by Professor Kevin Hammond. He is pictured with second supervisor Dr Christopher Brown, Internal examiner Dr Susmit Sarkar and external examiner Professor Susan Eisenbach from Imperial College, London.
Functional Programming
Towards Refinement by Resolution in Dependent Type Theory – FrantiĊĦek Farka
Event details
- When: 9th November 2017 12:00 - 13:00
- Where: Cole 1.33b
- Format: Talk
Abstract
Dependent types are increasingly used in functional programming languages. The surface syntax of dependent types, as seen by a programmer, is elaborated by a compiler into an internal, type-theoretic representation. In order to perform this step, the compiler needs to infer a nontrivial amount of information to successfully type-check the internal representation. This process—type refinement—is complex, implementation dependent, and very few formal developments currently exist. We discuss a novel and simpler formalisation of type refinement in first order type theory with dependent types. We propose a translation of type-refinement problems to Horn-Clause logic with explicit proof-terms, using proof-relevant resolution as the type inference mechanism.
Thesis Summary Presentation – Adam Barwell
Event details
- When: 2nd November 2017 12:00 - 13:00
- Where: Cole 1.33b
- Format: Talk
Adam Barwell (adb23) will be presenting a summary of his recently submitted thesis.