default search action
Andrew 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
2020 – today
- 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) - 2021
- [c46]Andrew M. Pitts, S. C. Steenkamp
Constructing Initial Algebras Using Inflationary Iteration. ACT 2021: 88-102 - [i13]Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp:
Quotients, inductive types, and quotient inductive types. CoRR abs/2101.02994 (2021) - 2020
- [j26]Lars Birkedal, Ranald Clouston, Bassel Mannaa
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) - [c45]Marcelo P. Fiore
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
2010 – 2019
- 2019
- [j24]Ian Orton, Andrew M. Pitts:
Models of Type Theory Based on Moore Paths. Log. Methods Comput. Sci. 15(1) (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
- [j23]Ian Orton, Andrew M. Pitts:
Axioms for Modelling Cubical Type Theory in a Topos. Log. Methods Comput. Sci. 14(4) (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 - [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
- [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 - [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) - 2016
- [j22]Andrew M. Pitts:
Nominal techniques. ACM SIGLOG News 3(1): 57-72 (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
- [j21]Andrew M. Pitts:
Gödel Prize 2016 - Call for Nominations. Bull. EATCS 117 (2015) - [c38]Andrew M. Pitts
Names and Symmetry in Computer Science (Invited Tutorial). LICS 2015: 21-22 - [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] - 2014
- [j20]Steffen Lösch, Andrew M. Pitts
Denotational Semantics with Nominal Scott Domains. J. ACM 61(4): 27:1-27:46 (2014) - [c37]Andrew M. Pitts:
Nominal Presentation of Cubical Sets Models of Type Theory. TYPES 2014: 202-220 - [c36]Andrew M. Pitts
A Dependent Type Theory with Abstractable Names. LSFA 2014: 19-50 - [i5]Andrew M. Pitts:
An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets. CoRR abs/1401.7807 (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) - [c35]Steffen Lösch, Andrew M. Pitts
Full abstraction for nominal Scott domains. POPL 2013: 3-14 - [c34]Ki Yung Ahn
System F i . TLCA 2013: 15-30 - [i4]Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts:
Nominal Computation Theory (Dagstuhl Seminar 13422). Dagstuhl Reports 3(10): 58-71 (2013) - 2012
- [j18]Matthew R. Lakin, Andrew M. Pitts:
Encoding Abstract Syntax Without Fresh Names. J. Autom. Reason. 49(2): 115-140 (2012) - [p1]Andrew M. Pitts:
Howe's method for higher-order languages. Advanced Topics in Bisimulation and Coinduction 2012: 197-232 - [e6]Artur Czumaj, Kurt Mehlhorn, Andrew M. Pitts
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
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] - 2011
- [j17]Andrew M. Pitts
Structural recursion with locally scoped names. J. Funct. Program. 21(3): 235-286 (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 - [i3]Andrew M. Pitts:
Step-Indexed Biorthogonality: a Tutorial Example. Modelling, Controlling and Reasoning About State 2010
2000 – 2009
- 2009
- [c31]Matthew R. Lakin, Andrew M. Pitts:
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. ESOP 2009: 47-61 - 2008
- [j16]Andrew M. Pitts
Generative Unbinding of Names. Log. Methods Comput. Sci. 4(1) (2008) - [i2]Andrew M. Pitts, Mark R. Shinwell:
Generative Unbinding of Names. CoRR abs/0801.1251 (2008) - 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 - 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) - [c26]Andrew M. Pitts:
Alpha-Structural Recursion and Induction. TPHOLs 2005: 17-34 - 2004
- [j13]Christian Urban, Andrew M. Pitts
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) - [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
- [j11]Murdoch Gabbay
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) - [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
- [j9]Andrew M. Pitts:
Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10(3): 321-359 (2000) - [c20]Andrew M. Pitts:
Operational Semantics and Program Equivalence. APPSEM 2000: 378-412 - [c19]Andrew M. Pitts
A Metalanguage for Programming with Bound Names Modulo Renaming. MPC 2000: 230-255 - [c18]Gavin M. Bierman, Andrew M. Pitts
Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion. HOOTS 2000: 70-88
1990 – 1999
- 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 - [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] - 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) - [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
- [j7]Andrew M. Pitts:
A Note on Logical Relations Between Semantics and Syntax. Log. J. IGPL 5(4): 589-601 (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 - [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] - 1996
- [j6]Andrew M. Pitts:
Relational Properties of Domains. Inf. Comput. 127(2): 66-90 (1996) - [c10]Andrew M. Pitts
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
- [j5]Andrew M. Pitts:
A co-Induction Principle for Recursively Defined Domains. Theor. Comput. Sci. 124(2): 195-219 (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 - [i1]Andrew M. Pitts:
Bisimulation and Co-induction (Tutorial). LICS 1993: 2-3 - 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) - 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] - 1990
- [c3]Roy L. Crole, Andrew M. Pitts:
New Foundations for Fixpoint Computations. LICS 1990: 489-497
1980 – 1989
- 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) - [c2]Andrew M. Pitts:
Non-trivial Power Types Can't Be Subtypes of Polymorphic Types. LICS 1989: 6-13 - [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] - 1987
- [c1]Andrew M. Pitts:
Polymorphism is Set Theoretic, Constructively. Category Theory and Computer Science 1987: 12-39
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 2024-05-02 20:55 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: