Andrew M. Pitts

According to our database, Andrew M. Pitts authored at least 72 papers between 1987 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Locally Nameless Sets.

Andrew M. Pitts

Proc. ACM Program. Lang., January, 2023

2022

Quotients, inductive types, and quotient inductive types.

Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp

Log. Methods Comput. Sci., 2022

2021

Constructing Initial Algebras Using Inflationary Iteration.

Andrew M. Pitts, S. C. Steenkamp

Proceedings of the Fourth International Conference on Applied Category Theory, 2021

2020

Typal Heterogeneous Equality Types.

Andrew M. Pitts

ACM Trans. Comput. Log., 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

Quotients in Dependent Type Theory (Invited Talk).

Andrew M. Pitts

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Constructing Infinitary Quotient-Inductive Types.

Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp

Proceedings of the Foundations of Software Science and Computation Structures, 2020

2019

Models of Type Theory Based on Moore Paths.

Ian Orton, Andrew M. Pitts

Log. Methods Comput. Sci., 2019

2018

Axioms for Modelling Cubical Type Theory in a Topos.

Ian Orton, Andrew M. Pitts

Log. Methods Comput. Sci., 2018

Modal Dependent Type Theory and Dependent Right Adjoints.

Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters

CoRR, 2018

Internal Universes in Models of Homotopy Type Theory.

Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017

Decomposing the Univalence Axiom.

Ian Orton, Andrew M. Pitts

Proceedings of the 23rd International Conference on Types for Proofs and Programs, 2017

2016

Nominal techniques.

Andrew M. Pitts

ACM SIGLOG News, 2016

Polinode: A web application for the collection and analysis of network data.

Andrew M. Pitts

Proceedings of the 2016 IEEE/ACM International Conference on Advances in Social Networks Analysis and Mining, 2016

2015

Gödel Prize 2016 - Call for Nominations.

Andrew M. Pitts

Bull. EATCS, 2015

Names and Symmetry in Computer Science (Invited Tutorial).

Andrew M. Pitts

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

Denotational Semantics with Nominal Scott Domains.

Steffen Lösch, Andrew M. Pitts

J. ACM, 2014

A Dependent Type Theory with Abstractable Names.

Andrew M. Pitts, Justus Matthiesen, Jasper Derikx

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets.

Andrew M. Pitts

CoRR, 2014

Nominal Presentation of Cubical Sets Models of Type Theory.

Andrew M. Pitts

Proceedings of the 20th International Conference on Types for Proofs and Programs, 2014

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 Computation Theory (Dagstuhl Seminar 13422).

Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts

Dagstuhl Reports, 2013

System F _<i>i</i>.

Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

Full abstraction for nominal Scott domains.

Steffen Lösch, Andrew M. Pitts

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

2012

Encoding Abstract Syntax Without Fresh Names.

Matthew R. Lakin, Andrew M. Pitts

J. Autom. Reason., 2012

Howe's method for higher-order languages.

Andrew M. Pitts

Proceedings of the Advanced Topics in Bisimulation and Coinduction., 2012

2011

Structural recursion with locally scoped names.

Andrew M. Pitts

J. Funct. Program., 2011

Relating Two Semantics of Locally Scoped Names.

Steffen Lösch, Andrew M. Pitts

Proceedings of the Computer Science Logic, 2011

2010

Nominal system T.

Andrew M. Pitts

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Step-Indexed Biorthogonality: a Tutorial Example.

Andrew M. Pitts

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

2009

Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming.

Matthew R. Lakin, Andrew M. Pitts

Proceedings of the Programming Languages and Systems, 2009

2008

Generative Unbinding of Names.

Andrew M. Pitts, Mark R. Shinwell

Log. Methods Comput. Sci., 2008

2007

Nominal Equational Logic.

Ranald Alexander Clouston, Andrew M. Pitts

Proceedings of the Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin, 2007

A Metalanguage for Structural Operational Semantics.

Matthew R. Lakin, Andrew M. Pitts

Proceedings of the Eighth Symposium on Trends in Functional Programming, 2007

Techniques for Contextual Equivalence in Higher-Order, Typed Languages.

Andrew M. Pitts

Proceedings of the Programming Languages and Systems, 2007

2006

Alpha-structural recursion and induction.

Andrew M. Pitts

J. ACM, 2006

2005

On a monadic semantics for freshness.

Mark R. Shinwell, Andrew M. Pitts

Theor. Comput. Sci., 2005

2004

Nominal unification.

Christian Urban, Andrew M. Pitts, Murdoch Gabbay

Theor. Comput. Sci., 2004

2003

Nominal logic, a first order theory of names and binding.

Andrew M. Pitts

Inf. Comput., 2003

FreshML: programming with binders made simple.

Mark R. Shinwell, Andrew M. Pitts, Murdoch Gabbay

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Nominal Unificaiton.

Christian Urban, Andrew M. Pitts, Murdoch Gabbay

Proceedings of the Computer Science Logic, 17th International Workshop, 2003

2002

A New Approach to Abstract Syntax with Variable Binding.

Murdoch Gabbay, Andrew M. Pitts

Formal Aspects Comput., 2002

Equivariant Syntax and Semantics.

Andrew M. Pitts

Proceedings of the Automata, Languages and Programming, 29th International Colloquium, 2002

2001

A Fresh Approach to Representing Syntax with Static Binders in Functional Programming.

Andrew M. Pitts

Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP '01), 2001

2000

Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion.

Gavin M. Bierman, Andrew M. Pitts, Claudio V. Russo

Proceedings of the 4th International Workshop on Higher Order Operational Techniques in Semantics, 2000

A Metalanguage for Programming with Bound Names Modulo Renaming.

Andrew M. Pitts, Murdoch Gabbay

Proceedings of the Mathematics of Program Construction, 5th International Conference, 2000

Operational Semantics and Program Equivalence.

Andrew M. Pitts

Proceedings of the Applied Semantics, International Summer School, 2000

1999

Tripos Theory in Retrospect.

Andrew M. Pitts

Proceedings of the Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30, 1999

Preface.

Andrew D. Gordon, Andrew M. Pitts

Proceedings of the Third Workshop on Higher-Order Operational Techniques in Semantics, 1999

A New Approach to Abstract Syntax Involving Binders.

Murdoch Gabbay, Andrew M. Pitts

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998

Process Calculus Based Upon Evaluation to Committed Form.

Andrew M. Pitts, Joshua R. X. Ross

Theor. Comput. Sci., 1998

Operational Versus Denotational Methods in the Semantics of Higher Order Languages.

Andrew M. Pitts

Proceedings of the Principles of Declarative Programming, 10th International Symposium, 1998

Existential Types: Logical Relations and Operational Equivalence.

Andrew M. Pitts

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

1997

A Note on Logical Relations Between Semantics and Syntax.

Andrew M. Pitts

Log. J. IGPL, 1997

Parametric Polymorphism and Operational Equivalence.

Andrew M. Pitts

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

Preface.

Andrew D. Gordon, Andrew M. Pitts, Carolyn L. Talcott

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

1996

Relational Properties of Domains.

Andrew M. Pitts

Inf. Comput., 1996

Reasoning about Local Variables with Operationally-Based Logical Relations.

Andrew M. Pitts

Proceedings of the Proceedings, 1996

1995

A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML.

Eike Ritter, Andrew M. Pitts

Proceedings of the Typed Lambda Calculi and Applications, 1995

1994

A co-Induction Principle for Recursively Defined Domains.

Andrew M. Pitts

Theor. Comput. Sci., 1994

Completeness and Continuity Properties of Applicative Bisimulation.

Andrew M. Pitts

Proceedings of the Proceedings for the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, 1994

1993

Computational Adequacy via "Mixed" Inductive Definitions.

Andrew M. Pitts

Proceedings of the Mathematical Foundations of Programming Semantics, 1993

Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?

Andrew M. Pitts, Ian David Bede Stark

Proceedings of the Mathematical Foundations of Computer Science 1993, 1993

Relational Properties of Recursively Defined Domains

Andrew M. Pitts

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1993

Bisimulation and Co-induction (Tutorial)

Andrew M. Pitts

LICS, 1993

1992

New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and the FIX-Logic

Roy L. Crole, Andrew M. Pitts

Inf. Comput., June, 1992

On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic.

Andrew M. Pitts

J. Symb. Log., 1992

1990

New Foundations for Fixpoint Computations

Roy L. Crole, Andrew M. Pitts

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

1989

A note on russell's paradox in locally cartesian closed categories.

Andrew M. Pitts, Paul Taylor

Stud Logica, 1989

Conceptual Completeness for First-Order Intuitionistic Logic: An Application of Categorical Logic.

Andrew M. Pitts

Ann. Pure Appl. Log., 1989

Non-trivial Power Types Can't Be Subtypes of Polymorphic Types

Andrew M. Pitts

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1987

Polymorphism is Set Theoretic, Constructively.

Andrew M. Pitts

Proceedings of the Category Theory and Computer Science, 1987