default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAndrew M. Pitts
Person information
- affiliation: University of Cambridge, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2023
[j28]Andrew M. Pitts
:
Locally Nameless Sets. Proc. ACM Program. Lang. 7(POPL): 488-514 (2023)- 2022
- [j27]Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp:
Quotients, inductive types, and quotient inductive types. Log. Methods Comput. Sci. 18(2) (2022) - 2020
- [j26]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): 118-138 (2020) - [j25]Andrew M. Pitts:
Typal Heterogeneous Equality Types. ACM Trans. Comput. Log. 21(3): 25:1-25:10 (2020) - 2019
- [j24]Ian Orton, Andrew M. Pitts:
Models of Type Theory Based on Moore Paths. Log. Methods Comput. Sci. 15(1) (2019) - 2018
- [j23]Ian Orton, Andrew M. Pitts:
Axioms for Modelling Cubical Type Theory in a Topos. Log. Methods Comput. Sci. 14(4) (2018) - 2016
- [j22]Andrew M. Pitts:
Nominal techniques. ACM SIGLOG News 3(1): 57-72 (2016) - 2015
- [j21]Andrew M. Pitts:
Gödel Prize 2016 - Call for Nominations. Bull. EATCS 117 (2015) - 2014
- [j20]Steffen Lösch, Andrew M. Pitts:
Denotational Semantics with Nominal Scott Domains. J. ACM 61(4): 27:1-27:46 (2014) - 2013
- [j19]Matthew R. Lakin, Andrew M. Pitts:
Contextual equivalence for inductive definitions with binders in higher order typed functional programming. J. Funct. Program. 23(6): 658-700 (2013) - 2012
- [j18]Matthew R. Lakin, Andrew M. Pitts:
Encoding Abstract Syntax Without Fresh Names. J. Autom. Reason. 49(2): 115-140 (2012) - 2011
- [j17]Andrew M. Pitts:
Structural recursion with locally scoped names. J. Funct. Program. 21(3): 235-286 (2011) - 2008
- [j16]Andrew M. Pitts, Mark R. Shinwell:
Generative Unbinding of Names. Log. Methods Comput. Sci. 4(1) (2008) - 2006
- [j15]Andrew M. Pitts:
Alpha-structural recursion and induction. J. ACM 53(3): 459-506 (2006) - 2005
- [j14]Mark R. Shinwell, Andrew M. Pitts:
On a monadic semantics for freshness. Theor. Comput. Sci. 342(1): 28-55 (2005) - 2004
- [j13]Christian Urban, Andrew M. Pitts, Murdoch Gabbay:
Nominal unification. Theor. Comput. Sci. 323(1-3): 473-497 (2004) - 2003
- [j12]Andrew M. Pitts:
Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2): 165-193 (2003) - 2002
- [j11]Murdoch Gabbay, Andrew M. Pitts:
A New Approach to Abstract Syntax with Variable Binding. Formal Aspects Comput. 13(3-5): 341-363 (2002) - [j10]Andrew M. Pitts:
Tripos Theory in Retrospect. Math. Struct. Comput. Sci. 12(3): 265-279 (2002) - 2000
- [j9]Andrew M. Pitts:
Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10(3): 321-359 (2000) - 1998
- [j8]Andrew M. Pitts, Joshua R. X. Ross:
Process Calculus Based Upon Evaluation to Committed Form. Theor. Comput. Sci. 195(2): 155-182 (1998) - 1997
- [j7]Andrew M. Pitts:
A Note on Logical Relations Between Semantics and Syntax. Log. J. IGPL 5(4): 589-601 (1997) - 1996
- [j6]Andrew M. Pitts:
Relational Properties of Domains. Inf. Comput. 127(2): 66-90 (1996) - 1994
- [j5]Andrew M. Pitts:
A co-Induction Principle for Recursively Defined Domains. Theor. Comput. Sci. 124(2): 195-219 (1994) - 1992
- [j4]Roy L. Crole, Andrew M. Pitts:
New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and the FIX-Logic. Inf. Comput. 98(2): 171-210 (1992) - [j3]Andrew M. Pitts:
On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic. J. Symb. Log. 57(1): 33-52 (1992) - 1989
- [j2]Andrew M. Pitts:
Conceptual Completeness for First-Order Intuitionistic Logic: An Application of Categorical Logic. Ann. Pure Appl. Log. 41(1): 33-81 (1989) - [j1]Andrew M. Pitts, Paul Taylor:
A note on russell's paradox in locally cartesian closed categories. Stud Logica 48(3): 377-387 (1989)
Conference and Workshop Papers
- 2021
- [c46]Andrew M. Pitts, S. C. Steenkamp:
Constructing Initial Algebras Using Inflationary Iteration. ACT 2021: 88-102 - 2020
- [c45]Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp:
Constructing Infinitary Quotient-Inductive Types. FoSSaCS 2020: 257-276 - [c44]Andrew M. Pitts:
Quotients in Dependent Type Theory (Invited Talk). FSCD 2020: 3:1-3:2 - 2018
- [c43]Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters:
Internal Universes in Models of Homotopy Type Theory. FSCD 2018: 22:1-22:17 - 2017
- [c42]Ian Orton, Andrew M. Pitts:
Models of Type Theory Based on Moore Paths. FSCD 2017: 28:1-28:16 - [c41]Ian Orton, Andrew M. Pitts:
Decomposing the Univalence Axiom. TYPES 2017: 6:1-6:19 - 2016
- [c40]Andrew M. Pitts:
Polinode: A web application for the collection and analysis of network data. ASONAM 2016: 1422-1425 - [c39]Ian Orton, Andrew M. Pitts:
Axioms for Modelling Cubical Type Theory in a Topos. CSL 2016: 24:1-24:19 - 2015
- [c38]Andrew M. Pitts:
Names and Symmetry in Computer Science (Invited Tutorial). LICS 2015: 21-22 - 2014
- [c37]Andrew M. Pitts:
Nominal Presentation of Cubical Sets Models of Type Theory. TYPES 2014: 202-220 - [c36]Andrew M. Pitts, Justus Matthiesen, Jasper Derikx:
A Dependent Type Theory with Abstractable Names. LSFA 2014: 19-50 - 2013
- [c35]Steffen Lösch, Andrew M. Pitts:
Full abstraction for nominal Scott domains. POPL 2013: 3-14 - [c34]Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts:
System F i . TLCA 2013: 15-30 - 2011
- [c33]Steffen Lösch, Andrew M. Pitts:
Relating Two Semantics of Locally Scoped Names. CSL 2011: 396-411 - 2010
- [c32]Andrew M. Pitts:
Nominal system T. POPL 2010: 159-170 - 2009
- [c31]Matthew R. Lakin, Andrew M. Pitts:
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. ESOP 2009: 47-61 - 2007
- [c30]Andrew M. Pitts:
Techniques for Contextual Equivalence in Higher-Order, Typed Languages. ESOP 2007: 1 - [c29]Andrew M. Pitts, Mark R. Shinwell:
Generative unbinding of names. POPL 2007: 85-95 - [c28]Matthew R. Lakin, Andrew M. Pitts:
A Metalanguage for Structural Operational Semantics. Trends in Functional Programming 2007: 19-35 - [c27]Ranald Alexander Clouston, Andrew M. Pitts:
Nominal Equational Logic. Computation, Meaning, and Logic 2007: 223-257 - 2005
- [c26]Andrew M. Pitts:
Alpha-Structural Recursion and Induction. TPHOLs 2005: 17-34 - 2003
- [c25]Christian Urban, Andrew M. Pitts, Murdoch Gabbay:
Nominal Unificaiton. CSL 2003: 513-527 - [c24]Mark R. Shinwell, Andrew M. Pitts, Murdoch Gabbay:
FreshML: programming with binders made simple. ICFP 2003: 263-274 - 2002
- [c23]Andrew M. Pitts:
Equivariant Syntax and Semantics. ICALP 2002: 32-36 - 2001
- [c22]Andrew M. Pitts:
A Fresh Approach to Representing Syntax with Static Binders in Functional Programming. ICFP 2001: 1 - [c21]Andrew M. Pitts:
Nominal Logic: A First Order Theory of Names and Binding. TACS 2001: 219-242 - 2000
- [c20]Andrew M. Pitts:
Operational Semantics and Program Equivalence. APPSEM 2000: 378-412 - [c19]Andrew M. Pitts, Murdoch Gabbay:
A Metalanguage for Programming with Bound Names Modulo Renaming. MPC 2000: 230-255 - [c18]Gavin M. Bierman, Andrew M. Pitts, Claudio V. Russo:
Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion. HOOTS 2000: 70-88 - 1999
- [c17]Murdoch Gabbay, Andrew M. Pitts:
A New Approach to Abstract Syntax Involving Binders. LICS 1999: 214-224 - [c16]Andrew D. Gordon, Andrew M. Pitts:
Preface. HOOTS 1999: 1-2 - [c15]Andrew M. Pitts:
Tripos Theory in Retrospect. Realizability Semantics and Applications@FLoC 1999: 111-127 - 1998
- [c14]Andrew M. Pitts:
Existential Types: Logical Relations and Operational Equivalence. ICALP 1998: 309-326 - [c13]Andrew M. Pitts:
Operational Versus Denotational Methods in the Semantics of Higher Order Languages. PLILP/ALP 1998: 282-283 - 1997
- [c12]Andrew D. Gordon, Andrew M. Pitts, Carolyn L. Talcott:
Preface. HOOTS 1997: 1 - [c11]Andrew M. Pitts:
Parametric Polymorphism and Operational Equivalence. HOOTS 1997: 2-27 - 1996
- [c10]Andrew M. Pitts, Joshua R. X. Ross:
Process Calculus Based upon Evaluation to Committed Form. CONCUR 1996: 18-33 - [c9]Andrew M. Pitts:
Reasoning about Local Variables with Operationally-Based Logical Relations. LICS 1996: 152-163 - 1995
- [c8]Eike Ritter, Andrew M. Pitts:
A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML. TLCA 1995: 397-413 - 1994
- [c7]Andrew M. Pitts:
Completeness and Continuity Properties of Applicative Bisimulation. Theory and Formal Methods 1994: 61 - 1993
- [c6]Andrew M. Pitts:
Relational Properties of Recursively Defined Domains. LICS 1993: 86-97 - [c5]Andrew M. Pitts, Ian David Bede Stark:
Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? MFCS 1993: 122-141 - [c4]Andrew M. Pitts:
Computational Adequacy via "Mixed" Inductive Definitions. MFPS 1993: 72-82 - 1990
- [c3]Roy L. Crole, Andrew M. Pitts:
New Foundations for Fixpoint Computations. LICS 1990: 489-497 - 1989
- [c2]Andrew M. Pitts:
Non-trivial Power Types Can't Be Subtypes of Polymorphic Types. LICS 1989: 6-13 - 1987
- [c1]Andrew M. Pitts:
Polymorphism is Set Theoretic, Constructively. Category Theory and Computer Science 1987: 12-39
Parts in Books or Collections
- 2012
- [p1]Andrew M. Pitts:
Howe's method for higher-order languages. Advanced Topics in Bisimulation and Coinduction 2012: 197-232
Editorship
- 2015
- [e7]Andrew M. Pitts:
Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science 9034, Springer 2015, ISBN 978-3-662-46677-3 [contents] - 2012
- [e6]Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, Roger Wattenhofer:
Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part I. Lecture Notes in Computer Science 7391, Springer 2012, ISBN 978-3-642-31593-0 [contents] - [e5]Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts, Roger Wattenhofer:
Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II. Lecture Notes in Computer Science 7392, Springer 2012, ISBN 978-3-642-31584-8 [contents] - 1999
- [e4]Andrew D. Gordon, Andrew M. Pitts:
Third Workshop on Higher-Order Operational Techniques in Semantics, HOOTS 1999, Paris, France, September 30 - October 1, 1999. Electronic Notes in Theoretical Computer Science 26, Elsevier 1999 [contents] - 1997
- [e3]Andrew D. Gordon, Andrew M. Pitts, Carolyn L. Talcott:
Second Workshop on Higher-Order Operational Techniques in Semantics, HOOTS 1997, Stanford, CA, USA, December 8-12, 1997. Electronic Notes in Theoretical Computer Science 10, Elsevier 1997 [contents] - 1991
- [e2]David H. Pitt, Pierre-Louis Curien, Samson Abramsky, Andrew M. Pitts, Axel Poigné, David E. Rydeheard:
Category Theory and Computer Science, 4th International Conference, Paris, France, September 3-6, 1991, Proceedings. Lecture Notes in Computer Science 530, Springer 1991, ISBN 3-540-54495-X [contents] - 1989
- [e1]David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné:
Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings. Lecture Notes in Computer Science 389, Springer 1989, ISBN 3-540-51662-X [contents]
Informal and Other Publications
- 2021
- [i13]Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp:
Quotients, inductive types, and quotient inductive types. CoRR abs/2101.02994 (2021) - 2019
- [i12]Andrew M. Pitts:
Typal Heterogeneous Equality Types. CoRR abs/1907.07501 (2019) - [i11]Marcelo Fiore, Andrew M. Pitts, S. C. Steenkamp:
Constructing Infinitary Quotient-Inductive Types. CoRR abs/1911.06899 (2019) - 2018
- [i10]Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters:
Internal Universes in Models of Homotopy Type Theory. CoRR abs/1801.07664 (2018) - [i9]Ian Orton, Andrew M. Pitts:
Models of Type Theory Based on Moore Paths. CoRR abs/1802.05629 (2018) - [i8]Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters:
Modal Dependent Type Theory and Dependent Right Adjoints. CoRR abs/1804.05236 (2018) - 2017
- [i7]Ian Orton, Andrew M. Pitts:
Axioms for Modelling Cubical Type Theory in a Topos. CoRR abs/1712.04864 (2017) - [i6]Ian Orton, Andrew M. Pitts:
Decomposing the Univalence Axiom. CoRR abs/1712.04890 (2017) - 2014
- [i5]Andrew M. Pitts:
An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets. CoRR abs/1401.7807 (2014) - 2013
- [i4]Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts:
Nominal Computation Theory (Dagstuhl Seminar 13422). Dagstuhl Reports 3(10): 58-71 (2013) - 2010
- [i3]Andrew M. Pitts:
Step-Indexed Biorthogonality: a Tutorial Example. Modelling, Controlling and Reasoning About State 2010 - 2008
- [i2]Andrew M. Pitts, Mark R. Shinwell:
Generative Unbinding of Names. CoRR abs/0801.1251 (2008) - 1993
- [i1]Andrew M. Pitts:
Bisimulation and Co-induction (Tutorial). LICS 1993: 2-3
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-07-17 01:13 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
