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

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

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

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

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

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

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

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

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

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

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

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

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 | 111 | 2003 |

Categorical logic AM Pitts Clarendon Press, 2001 | 111 | 2001 |

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

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 | 110 | 1992 |

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

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

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