Type Systems for Nominal Terms

Abstract

This thesis concerns types systems for nominal terms, a new syntax, close to
informal practice, for representing and reasoning about formal languages that
use binders.
Nominal techniques allow a rst-order approach to binding in formal languages,
providing direct access to both binders and bound variables and a formal axiomatisation of -equivalence. This approach is promising, not least because
it has been shown that unication and matching of nominal representations
is both decidable and tractable, giving rise to nominal models of computation
and programming languages. Nominal terms, a nominal extension of rst-order
terms, are now well studied, particularly in the context of equational reasoning.
However, type systems for nominal terms have not yet been extensively
researched.
The development of type systems for nominal terms allows the application of
the nominal approach to binding to the areas of specication and verication.
Programming languages and environments based upon certifying type systems
facilitate formal descriptions of operational semantics and the implementation
of ecient compilers. Such features are increasingly important, particularly in
critical domains where mathematical certainty is a necessity, such as medicine,
telecommunications, transport and defence.
This work rst denes three variations on a simple type system for nominal
terms in the style of Church's simply typed lambda calculus. An ML-style
polymorphic type system is then studied for which a type inference algorithm
is provided and implemented. This type system is then applied to equational
theories. Two formulations of typed rewriting are presented, one more expressive and one more ecient. Finally, a dependent type system is given for
nominal terms extended with atom substitution, with a view to developing a
nominal logical framework.

Date of Award	2014
Original language	English
Awarding Institution	King's College London
Supervisor	Maribel Fernandez (Supervisor)