Student research opportunities
Theory of Co-algebraic Types with Binders
Project Code: CECS_105
This project is available at the following levels:
PhD
Please note that this project is only for higher degree (postgraduate) applicants.
Keywords:
nominal theory, mechanisation, theorem-proving
Supervisor:
Dr Michael NorrishOutline:
Researchers in the area of programming language semantics have long been exercised by the problems thrown up the notions of binders and α-equivalence. Some progress has been made recently, but focussing on types that are quotients of algebraic or inductive types, where values are finite in size. Co-algebraic types are potentially infinite in size, which means that assumptions like the one that a value only has finitely many free variables will no longer hold.
Developing a theory of co-algebraic types with binders would probably involve proving co-induction and co-recursion principles for these types, and demonstrating their utility in proofs drawn from the literature. One possible example would be the Boehm tree, which is used in the theory of the λ-calculus.
