Polymorphism is Set Theoretic, Constructively. - Andrew M. Pitts (Category Theory and Computer Science, 1987)

Non-trivial Power Types Can't Be Subtypes of Polymorphic Types - Andrew M. Pitts (LICS, 1989)

Conceptual Completeness for First-Order Intuitionistic Logic: An Application of Categorical Logic. - Andrew M. Pitts (Ann. Pure Appl. Log., 1989)

A note on russell's paradox in locally cartesian closed categories. - Andrew M. Pitts; Paul Taylor (Stud Logica, 1989)

New Foundations for Fixpoint Computations - Roy L. Crole; Andrew M. Pitts (LICS, 1990)

On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. - Andrew M. Pitts (J. Symb. Log., 1992)

New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and the FIX-Logic - Roy L. Crole; Andrew M. Pitts (Inf. Comput., 1992)

Bisimulation and Co-induction (Tutorial) - Andrew M. Pitts (LICS, 1993)

Relational Properties of Recursively Defined Domains - Andrew M. Pitts (LICS, 1993)

Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? - Andrew M. Pitts; Ian David Bede Stark (MFCS, 1993)

Computational Adequacy via "Mixed" Inductive Definitions. - Andrew M. Pitts (MFPS, 1993)

Completeness and Continuity Properties of Applicative Bisimulation. - Andrew M. Pitts (Theory and Formal Methods, 1994)

A co-Induction Principle for Recursively Defined Domains. - Andrew M. Pitts (Theor. Comput. Sci., 1994)

A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML. - Eike Ritter; Andrew M. Pitts (TLCA, 1995)

Reasoning about Local Variables with Operationally-Based Logical Relations. - Andrew M. Pitts (LICS, 1996)

Relational Properties of Domains. - Andrew M. Pitts (Inf. Comput., 1996)

Preface. - Andrew D. Gordon 001; Andrew M. Pitts; Carolyn L. Talcott (HOOTS, 1997)

Parametric Polymorphism and Operational Equivalence. - Andrew M. Pitts (HOOTS, 1997)

A Note on Logical Relations Between Semantics and Syntax. - Andrew M. Pitts (Log. J. IGPL, 1997)

Existential Types: Logical Relations and Operational Equivalence. - Andrew M. Pitts (ICALP, 1998)

Operational Versus Denotational Methods in the Semantics of Higher Order Languages. - Andrew M. Pitts (PLILP/ALP, 1998)

Process Calculus Based Upon Evaluation to Committed Form. - Andrew M. Pitts; Joshua R. X. Ross (Theor. Comput. Sci., 1998)

A New Approach to Abstract Syntax Involving Binders. - Murdoch Gabbay; Andrew M. Pitts (LICS, 1999)

Preface. - Andrew D. Gordon 001; Andrew M. Pitts (HOOTS, 1999)

Tripos Theory in Retrospect. - Andrew M. Pitts (Realizability Semantics and Applications@FLoC, 1999)

Operational Semantics and Program Equivalence. - Andrew M. Pitts (APPSEM, 2000)

A Metalanguage for Programming with Bound Names Modulo Renaming. - Andrew M. Pitts; Murdoch Gabbay (MPC, 2000)

Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion. - Gavin M. Bierman; Andrew M. Pitts; Claudio V. Russo (HOOTS, 2000)

A Fresh Approach to Representing Syntax with Static Binders in Functional Programming. - Andrew M. Pitts (ICFP, 2001)

Equivariant Syntax and Semantics. - Andrew M. Pitts (ICALP, 2002)

A New Approach to Abstract Syntax with Variable Binding. - Murdoch Gabbay; Andrew M. Pitts (Formal Aspects Comput., 2002)

Nominal Unificaiton. - Christian Urban; Andrew M. Pitts; Murdoch Gabbay (CSL, 2003)

FreshML: programming with binders made simple. - Mark R. Shinwell; Andrew M. Pitts; Murdoch Gabbay (ICFP, 2003)

Nominal logic, a first order theory of names and binding. - Andrew M. Pitts (Inf. Comput., 2003)

Nominal unification. - Christian Urban; Andrew M. Pitts; Murdoch Gabbay (Theor. Comput. Sci., 2004)

On a monadic semantics for freshness. - Mark R. Shinwell; Andrew M. Pitts (Theor. Comput. Sci., 2005)

Alpha-structural recursion and induction. - Andrew M. Pitts (J. ACM, 2006)

Techniques for Contextual Equivalence in Higher-Order, Typed Languages. - Andrew M. Pitts (ESOP, 2007)

A Metalanguage for Structural Operational Semantics. - Matthew R. Lakin; Andrew M. Pitts (Trends in Functional Programming, 2007)

Nominal Equational Logic. - Ranald Alexander Clouston; Andrew M. Pitts (Computation, Meaning, and Logic, 2007)

Generative Unbinding of Names. - Andrew M. Pitts; Mark R. Shinwell (Log. Methods Comput. Sci., 2008)

Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. - Matthew R. Lakin; Andrew M. Pitts (ESOP, 2009)

Step-Indexed Biorthogonality: a Tutorial Example. - Andrew M. Pitts (Modelling, Controlling and Reasoning About State, 2010)

Nominal system T. - Andrew M. Pitts (POPL, 2010)

Relating Two Semantics of Locally Scoped Names. - Steffen Lösch; Andrew M. Pitts (CSL, 2011)

Structural recursion with locally scoped names. - Andrew M. Pitts (J. Funct. Program., 2011)

Howe's method for higher-order languages. - Andrew M. Pitts (Advanced Topics in Bisimulation and Coinduction, 2012)

Encoding Abstract Syntax Without Fresh Names. - Matthew R. Lakin; Andrew M. Pitts (J. Autom. Reason., 2012)

Full abstraction for nominal Scott domains. - Steffen Lösch; Andrew M. Pitts (POPL, 2013)

System F i . - Ki Yung Ahn; Tim Sheard; Marcelo P. Fiore; Andrew M. Pitts (TLCA, 2013)

Nominal Computation Theory (Dagstuhl Seminar 13422). - Mikolaj Bojanczyk; Bartek Klin; Alexander Kurz 001; Andrew M. Pitts (Dagstuhl Reports, 2013)

Contextual equivalence for inductive definitions with binders in higher order typed functional programming. - Matthew R. Lakin; Andrew M. Pitts (J. Funct. Program., 2013)

Nominal Presentation of Cubical Sets Models of Type Theory. - Andrew M. Pitts (TYPES, 2014)

An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets. - Andrew M. Pitts (CoRR, 2014)

A Dependent Type Theory with Abstractable Names. - Andrew M. Pitts; Justus Matthiesen; Jasper Derikx (LSFA, 2014)

Denotational Semantics with Nominal Scott Domains. - Steffen Lösch; Andrew M. Pitts (J. ACM, 2014)

Names and Symmetry in Computer Science (Invited Tutorial). - Andrew M. Pitts (LICS, 2015)

Gödel Prize 2016 - Call for Nominations. - Andrew M. Pitts (Bull. EATCS, 2015)

Polinode: A web application for the collection and analysis of network data. - Andrew M. Pitts (ASONAM, 2016)

Nominal techniques. - Andrew M. Pitts (ACM SIGLOG News, 2016)

Decomposing the Univalence Axiom. - Ian Orton; Andrew M. Pitts (TYPES, 2017)

Internal Universes in Models of Homotopy Type Theory. - Daniel R. Licata; Ian Orton; Andrew M. Pitts; Bas Spitters (FSCD, 2018)

Modal Dependent Type Theory and Dependent Right Adjoints. - Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (CoRR, 2018)

Axioms for Modelling Cubical Type Theory in a Topos. - Ian Orton; Andrew M. Pitts (Log. Methods Comput. Sci., 2018)

Models of Type Theory Based on Moore Paths. - Ian Orton; Andrew M. Pitts (Log. Methods Comput. Sci., 2019)

Constructing Infinitary Quotient-Inductive Types. - Marcelo P. Fiore; Andrew M. Pitts; S. C. Steenkamp (FoSSaCS, 2020)

Quotients in Dependent Type Theory (Invited Talk). - Andrew M. Pitts (FSCD, 2020)

Modal dependent type theory and dependent right adjoints. - Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (Math. Struct. Comput. Sci., 2020)

Typal Heterogeneous Equality Types. - Andrew M. Pitts (ACM Trans. Comput. Log., 2020)

Constructing Initial Algebras Using Inflationary Iteration. - Andrew M. Pitts; S. C. Steenkamp (ACT, 2021)

Quotients, inductive types, and quotient inductive types. - Marcelo P. Fiore; Andrew M. Pitts; S. C. Steenkamp (Log. Methods Comput. Sci., 2022)

Locally Nameless Sets. - Andrew M. Pitts (Proc. ACM Program. Lang., 2023)