Andrew M. Pitts

Publication Activity (10 Years)

Years Active: 1987-2023
Publications (10 Years): 23

Top Topics

Denotational Semantics

Theoretical Basis

Functional Programming

Top Venues

Log. Methods Comput. Sci.

Publications

Andrew M. Pitts
Locally Nameless Sets. Proc. ACM Program. Lang. 7 (POPL) (2023)
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
Quotients, inductive types, and quotient inductive types. Log. Methods Comput. Sci. 18 (2) (2022)
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
Quotients, inductive types, and quotient inductive types. CoRR (2021)
Andrew M. Pitts, S. C. Steenkamp
Constructing Initial Algebras Using Inflationary Iteration. CoRR (2021)
Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30 (2) (2020)
Andrew M. Pitts
Quotients in Dependent Type Theory (Invited Talk). FSCD (2020)
Andrew M. Pitts
Typal Heterogeneous Equality Types. ACM Trans. Comput. Log. 21 (3) (2020)
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
Constructing Infinitary Quotient-Inductive Types. FoSSaCS (2020)
Andrew M. Pitts
Typal Heterogeneous Equality Types. CoRR (2019)
Marcelo Fiore, Andrew M. Pitts, S. C. Steenkamp
Constructing Infinitary Quotient-Inductive Types. CoRR (2019)
Ian Orton, Andrew M. Pitts
Models of Type Theory Based on Moore Paths. Log. Methods Comput. Sci. 15 (1) (2019)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. CoRR (2018)
Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters
Modal Dependent Type Theory and Dependent Right Adjoints. CoRR (2018)
Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters
Internal Universes in Models of Homotopy Type Theory. FSCD (2018)
Ian Orton, Andrew M. Pitts
Models of Type Theory Based on Moore Paths. CoRR (2018)
Ian Orton, Andrew M. Pitts
Axioms for Modelling Cubical Type Theory in a Topos. Log. Methods Comput. Sci. 14 (4) (2018)
Ian Orton, Andrew M. Pitts
Decomposing the Univalence Axiom. TYPES (2017)
Ian Orton, Andrew M. Pitts
Models of Type Theory Based on Moore Paths. FSCD (2017)
Ian Orton, Andrew M. Pitts
Axioms for Modelling Cubical Type Theory in a Topos. CoRR (2017)
Ian Orton, Andrew M. Pitts
Decomposing the Univalence Axiom. CoRR (2017)
Andrew M. Pitts
Polinode: A web application for the collection and analysis of network data. ASONAM (2016)
Ian Orton, Andrew M. Pitts
Axioms for Modelling Cubical Type Theory in a Topos. CSL (2016)
Andrew M. Pitts
Nominal techniques. ACM SIGLOG News 3 (1) (2016)
Andrew M. Pitts
Names and Symmetry in Computer Science (Invited Tutorial). LICS (2015)
Andrew M. Pitts
Gödel Prize 2016 - Call for Nominations. Bull. EATCS 117 (2015)
Andrew M. Pitts, Justus Matthiesen, Jasper Derikx
A Dependent Type Theory with Abstractable Names. LSFA (2014)
Steffen Lösch, Andrew M. Pitts
Denotational Semantics with Nominal Scott Domains. J. ACM 61 (4) (2014)
Andrew M. Pitts
Nominal Presentation of Cubical Sets Models of Type Theory. TYPES (2014)
Andrew M. Pitts
An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets. CoRR (2014)
Steffen Lösch, Andrew M. Pitts
Full abstraction for nominal Scott domains. POPL (2013)
Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts
Nominal Computation Theory (Dagstuhl Seminar 13422). Dagstuhl Reports 3 (10) (2013)
Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts
. TLCA (2013)
Matthew R. Lakin, Andrew M. Pitts
Contextual equivalence for inductive definitions with binders in higher order typed functional programming. J. Funct. Program. 23 (6) (2013)
Matthew R. Lakin, Andrew M. Pitts
Encoding Abstract Syntax Without Fresh Names. J. Autom. Reason. 49 (2) (2012)
Andrew M. Pitts
Structural recursion with locally scoped names. J. Funct. Program. 21 (3) (2011)
Steffen Lösch, Andrew M. Pitts
Relating Two Semantics of Locally Scoped Names. CSL (2011)
Andrew M. Pitts
Nominal system T. POPL (2010)
Andrew M. Pitts
Step-Indexed Biorthogonality: a Tutorial Example. Modelling, Controlling and Reasoning About State (2010)
Matthew R. Lakin, Andrew M. Pitts
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. ESOP (2009)
Andrew M. Pitts, Mark R. Shinwell
Generative Unbinding of Names CoRR (2008)
Andrew M. Pitts, Mark R. Shinwell
Generative Unbinding of Names. Log. Methods Comput. Sci. 4 (1) (2008)
Andrew M. Pitts
Techniques for Contextual Equivalence in Higher-Order, Typed Languages. ESOP (2007)
Andrew M. Pitts, Mark R. Shinwell
Generative unbinding of names. POPL (2007)
Matthew R. Lakin, Andrew M. Pitts
A Metalanguage for Structural Operational Semantics. Trends in Functional Programming (2007)
Ranald Alexander Clouston, Andrew M. Pitts
Nominal Equational Logic. Electron. Notes Theor. Comput. Sci. 172 (2007)
Andrew M. Pitts
Alpha-structural recursion and induction. J. ACM 53 (3) (2006)
Mark R. Shinwell, Andrew M. Pitts
On a monadic semantics for freshness. Theor. Comput. Sci. 342 (1) (2005)
Andrew M. Pitts
Alpha-Structural Recursion and Induction. TPHOLs (2005)
Christian Urban, Andrew M. Pitts, Murdoch Gabbay
Nominal unification. Theor. Comput. Sci. 323 (1-3) (2004)
Mark R. Shinwell, Andrew M. Pitts, Murdoch Gabbay
FreshML: programming with binders made simple. ICFP (2003)
Andrew M. Pitts
Nominal logic, a first order theory of names and binding. Inf. Comput. 186 (2) (2003)
Christian Urban, Andrew M. Pitts, Murdoch Gabbay
Nominal Unificaiton. CSL (2003)
Andrew M. Pitts, Murdoch James Gabbay, Mark R. Shinwell
FreshML: programming with binders made simple. SIGPLAN Notices (2003)
Murdoch Gabbay, Andrew M. Pitts
A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput. 13 (3-5) (2002)
Andrew M. Pitts
Equivariant Syntax and Semantics. ICALP (2002)
Andrew M. Pitts
Tripos Theory in Retrospect. Math. Struct. Comput. Sci. 12 (3) (2002)
Andrew M. Pitts
Nominal Logic: A First Order Theory of Names and Binding. TACS (2001)
Andrew M. Pitts
A Fresh Approach to Representing Syntax with Static Binders in Functional Programming. ICFP (2001)
Gavin M. Bierman, Andrew M. Pitts, Claudio V. Russo
Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion. Electron. Notes Theor. Comput. Sci. 41 (3) (2000)
Andrew M. Pitts
Operational Semantics and Program Equivalence. APPSEM (2000)
Andrew M. Pitts, Murdoch Gabbay
A Metalanguage for Programming with Bound Names Modulo Renaming. MPC (2000)
Andrew M. Pitts
Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10 (3) (2000)
Andrew M. Pitts
Tripos Theory in Retrospect. Electron. Notes Theor. Comput. Sci. 23 (1) (1999)
Murdoch Gabbay, Andrew M. Pitts
A New Approach to Abstract Syntax Involving Binders. LICS (1999)
Andrew D. Gordon, Andrew M. Pitts
Preface. Electron. Notes Theor. Comput. Sci. 26 (1999)
Andrew M. Pitts
Operational Versus Denotational Methods in the Semantics of Higher Order Languages. PLILP/ALP (1998)
Andrew M. Pitts, Joshua R. X. Ross
Process Calculus Based Upon Evaluation to Committed Form. Theor. Comput. Sci. 195 (2) (1998)
Andrew M. Pitts
Existential Types: Logical Relations and Operational Equivalence. ICALP (1998)
Andrew D. Gordon, Andrew M. Pitts, Carolyn L. Talcott
Preface. Electron. Notes Theor. Comput. Sci. 10 (1997)
Andrew M. Pitts
A Note on Logical Relations Between Semantics and Syntax. Log. J. IGPL 5 (4) (1997)
Andrew M. Pitts
Parametric Polymorphism and Operational Equivalence. Electron. Notes Theor. Comput. Sci. 10 (1997)
Andrew M. Pitts, Joshua R. X. Ross
Process Calculus Based upon Evaluation to Committed Form. CONCUR (1996)
Andrew M. Pitts
Relational Properties of Domains. Inf. Comput. 127 (2) (1996)
Andrew M. Pitts
Reasoning about Local Variables with Operationally-Based Logical Relations. LICS (1996)
Eike Ritter, Andrew M. Pitts
A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML. TLCA (1995)
Andrew M. Pitts
A co-Induction Principle for Recursively Defined Domains. Theor. Comput. Sci. 124 (2) (1994)
Andrew M. Pitts
Completeness and Continuity Properties of Applicative Bisimulation. Theory and Formal Methods (1994)
Andrew M. Pitts
Computational Adequacy via "Mixed" Inductive Definitions. MFPS (1993)
Andrew M. Pitts
Relational Properties of Recursively Defined Domains LICS (1993)
Andrew M. Pitts, Ian David Bede Stark
Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? MFCS (1993)
Andrew M. Pitts
Bisimulation and Co-induction (Tutorial) LICS (1993)
Roy L. Crole, Andrew M. Pitts
New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and the FIX-Logic Inf. Comput. 98 (2) (1992)
Andrew M. Pitts
On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. J. Symb. Log. 57 (1) (1992)
Roy L. Crole, Andrew M. Pitts
New Foundations for Fixpoint Computations LICS (1990)
Andrew M. Pitts
Conceptual Completeness for First-Order Intuitionistic Logic: An Application of Categorical Logic. Ann. Pure Appl. Log. 41 (1) (1989)
Andrew M. Pitts, Paul Taylor
A note on russell's paradox in locally cartesian closed categories. Stud Logica 48 (3) (1989)
Andrew M. Pitts
Non-trivial Power Types Can't Be Subtypes of Polymorphic Types LICS (1989)
Andrew M. Pitts
Polymorphism is Set Theoretic, Constructively. Category Theory and Computer Science (1987)