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

Nominal logic, a first order theory of names and binding AM Pitts Information and computation 186 (2), 165-193, 2003 | 432 | 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, 1993 | 202 | 1993 |

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

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

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

Categorical logic AM Pitts University of Cambridge, Computer Laboratory, 1995 | 175 | 1995 |

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

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

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

Tripos theory JME Hyland, PT Johnstone, AM Pitts Mathematical Proceedings of the Cambridge philosophical society 88 (02), 205-232, 1980 | 152 | 1980 |

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

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

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

On an interpretation of second order quantification in first order intuitionistic propositional logic AM Pitts The Journal of Symbolic Logic 57 (01), 33-52, 1992 | 115 | 1992 |

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

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

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

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

7 Typed Operational Reasoning A Pitts | 72 | 2005 |