View Proposal

Proposer
James McKinna
Title
B"ohm trees
Goal
Description
B"ohm trees are infinite objects corresponding to the successive 'unfolding' of a term in lambda calculus; they can be regarded either as a possible semantics of lambda terms, or as an extended language of terms with extended notions of the usual reduction relations on lambda terms. This project, which can be appropriately scoped according to the level and skills of the student, is to study formal representations of lambda terms in a system such as the Agda implementation of type theory. Aspects of the theory of B"ohm trees include: * continuity properties (trees can be given a topology for which application and lambda abstraction are continuous) * extending the Standardisation theorem for ordinary lambda calculus to the extended reduction system on trees; * other topics as they may arise The interested student should have a good mathematical background; an interest in (the foundations of) programming languages; preferably direct experience in the form of our CS Foundations I and II courses
Resources
Background
Url
Difficulty Level
Challenging
Ethical Approval
None
Number Of Students
1
Supervisor
James McKinna
Keywords
Degrees
Back to List