Nominal logic for verification and security

Nominal abstract syntax is a recent and fruitful approach to formally defining syntax modulo alpha-equivalence. Nominal techniques are supported in the Nominal Isabelle system and some other tools (such as a logic programming language alphaProlog), which can (and have) been used to verify substantial systems, including dependent type theories such as LF and practical languages such as XQuery. I'd be interested in supervising research in any area related to nominal logic, type theory or mechanized metatheory. This could involve focusing on formalization of existing systems of interest, identifying opportunities for adapting automated reasoning (such as proof planning) to the nominal setting, or developing new, more constructive formalisms that could provide a foundation for adoption of nominal techniques in type-theoretic proof assistants such as Coq.

Recent developments such as Homotopy Type Theory could provide new avenues of attack on this problem, for example by making it possible to define the basic concepts of nominal logic in constructive type theories, using quotients.

Another application area of particular interest is Security. Nominal logic extends ordinary logic with special features for reasoning about names, particularly freshly introduced names with a particular scope (similar to nonces in cryptographic protocols). Thus nominal logics and type theory may form a good foundation for verification of security properties.

This work would be suitable for a student with a strong background in type theory, semantics, or automated reasoning.

Potential Supervisor:

James Cheney

Document Actions

• Print this