A new approach to abstract syntax with variable binding MJ Gabbay, AM Pitts Formal aspects of computing 13 (3-5), 341-363 | 663 | ∗ | 2002 |

Nominal logic, a first order theory of names and binding AM Pitts Information and computation 186 (2), 165-193 | 406 | | 2003 |

Observable properties of higher order functions that dynamically create local names, or: What's new? AM Pitts, IDB Stark Mathematical Foundations of Computer Science 1993, 122-141 | 198 | | 1993 |

Relational properties of domains AM Pitts Information and Computation 127 (2), 66-90 | 186 | | 1996 |

Operational reasoning for functions with local state AM Pitts, IDB Stark Higher order operational techniques in semantics, 227-273 | 175 | ∗ | 1998 |

FreshML: Programming with binders made simple MR Shinwell, AM Pitts, MJ Gabbay ACM SIGPLAN Notices 38 (9), 263-274 | 167 | | 2003 |

Parametric polymorphism and operational equivalence AM Pitts Mathematical Structures in Computer Science 10 (3), 321-359 | 158 | | 2000 |

Nominal unification C Urban, AM Pitts, MJ Gabbay Theoretical Computer Science 323 (1), 473-497 | 152 | | 2004 |

Operationally-based theories of program equivalence AM Pitts Semantics and Logics of Computation 14, 241 | 150 | | 1997 |

Polymorphism is set theoretic, constructively AM Pitts Category Theory and Computer Science, 12-39 | 145 | | 1987 |

A metalanguage for programming with bound names modulo renaming AM Pitts, MJ Gabbay Mathematics of Program Construction, 230-255 | 141 | | 2000 |

Tripos theory JME Hyland, PT Johnstone, AM Pitts Math. Proc. Camb. Phil. Soc 88 (205-232) | 141 | | 1980 |

The theory of constructions: Categorical semantics and topos-theoretic models JME Hyland, AM Pitts Contemporary Mathematics 92, 137-199 | 121 | | 1989 |

Categorical logic AM Pitts Clarendon Press | 110 | | 2001 |

A co-induction principle for recursively defined domains AM Pitts Theoretical Computer Science 124 (2), 195-219 | 110 | | 1994 |

MJ: An imperative core calculus for Java and Java with effects G Bierman, M Parkinson, A Pitts Technical Report 563, Cambridge University Computer Laboratory | 108 | | 2003 |

On an interpretation of second order quantification in first order intuitionistic propositional logic AM Pitts J. Symb. Log. 57 (1), 33-52 | 108 | | 1992 |

Alpha-structural recursion and induction AM Pitts Journal of the ACM (JACM) 53 (3), 459-506 | 78 | | 2006 |

Evaluation logic AM Pitts IV Higher Order Workshop, Banff 1990, 162-189 | 77 | | 1991 |

New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic RL Crole, AM Pitts Information and Computation 98 (2), 171-210 | 71 | | 1992 |