| 2020 | FOSSACS | Constructing Infinitary Quotient-Inductive Types. | Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp |
| 2020 | FSCD | Quotients in Dependent Type Theory (Invited Talk). | Andrew M. Pitts |
| 2016 | CSL | Axioms for Modelling Cubical Type Theory in a Topos. | Ian Orton, Andrew M. Pitts |
| 2015 | LICS | Names and Symmetry in Computer Science (Invited Tutorial). | Andrew M. Pitts |
| 2013 | POPL | Full abstraction for nominal Scott domains. | Steffen Lsch, Andrew M. Pitts |
| 2011 | CSL | Relating Two Semantics of Locally Scoped Names. | Steffen Lsch, Andrew M. Pitts |
| 2010 | POPL | Nominal system T. | Andrew M. Pitts |
| 2009 | ESOP | Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. | Matthew R. Lakin, Andrew M. Pitts |
| 2007 | ESOP | Techniques for Contextual Equivalence in Higher-Order, Typed Languages. | Andrew M. Pitts |
| 2007 | POPL | Generative unbinding of names. | Andrew M. Pitts, Mark R. Shinwell |
| 2003 | CSL | Nominal Unificaiton. | Christian Urban, Andrew M. Pitts, Murdoch Gabbay |
| 2003 | ICFP | FreshML: programming with binders made simple. | Mark R. Shinwell, Andrew M. Pitts, Murdoch Gabbay |
| 2002 | ICALP | Equivariant Syntax and Semantics. | Andrew M. Pitts |
| 2001 | ICFP | A Fresh Approach to Representing Syntax with Static Binders in Functional Programming. | Andrew M. Pitts |
| 2000 | MPC | A Metalanguage for Programming with Bound Names Modulo Renaming. | Andrew M. Pitts, Murdoch Gabbay |
| 1999 | LICS | A New Approach to Abstract Syntax Involving Binders. | Murdoch Gabbay, Andrew M. Pitts |
| 1998 | ICALP | Existential Types: Logical Relations and Operational Equivalence. | Andrew M. Pitts |
| 1996 | CONCUR | Process Calculus Based upon Evaluation to Committed Form. | Andrew M. Pitts, Joshua R. X. Ross |
| 1996 | LICS | Reasoning about Local Variables with Operationally-Based Logical Relations. | Andrew M. Pitts |
| 1993 | LICS | Bisimulation and Co-induction (Tutorial) | Andrew M. Pitts |
| 1993 | LICS | Relational Properties of Recursively Defined Domains | Andrew M. Pitts |
| 1993 | MFCS | Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? | Andrew M. Pitts, Ian David Bede Stark |
| 1993 | MFPS | Computational Adequacy via "Mixed" Inductive Definitions. | Andrew M. Pitts |
| 1990 | LICS | New Foundations for Fixpoint Computations | Roy L. Crole, Andrew M. Pitts |
| 1989 | LICS | Non-trivial Power Types Can't Be Subtypes of Polymorphic Types | Andrew M. Pitts |