 |
 |
 |
 |
|
|
||||
|
 |
Department of Computer Science & Technology Andrew Pitts |
|
|
||
|
||
| Department of Computer Science & Technology > Andrew Pitts |
Professor of Theoretical Computer Science
Fellow of Darwin College, Cambridge FACM FBCS CITP Contact
PublicationsResearchMy research makes use of techniques from category theory, mathematical logic and type theory to advance the foundations of programming language semantics and theorem proving systems. I have a long-standing interest in the semantics and logic of names, locality and binding. My aim is to develop mathematical models and methods which aid language design and the development of formal logics for specifying and reasoning about programs. I am particularly interested in higher-order typed programming languages and in dependently typed logics. 
Nominal Sets provide a promising new mathematical analysis of names in computer science that is based upon symmetry. They have applications to the syntax and semantics of programming language constructs that involve binding and localising the scope of names; to logics that underly systems for machine-assisted reasoning about programming language semantics; and to the automatic verification of process specifications in nominal calculi for concurrency (such as π-calculus). Nominal sets and their generalisations are being applied to automata theory over infinite alphabets with applications to querying XML and databases. Nominal sets also feature in recent work on the cubical sets model of Homotopy Type Theory and univalent foundations. Note: I am no longer taking on PhD students. (I am unable to do so because a compulsory retirement age of 67 has been introduced by the University of Cambridge for its academic staff, following the abolition of the default retirement age in April 2011.) TeachingLecture material for 2022/23 courses: Lecture material for old courses: |
|
|
|
|