Andrew M. Pitts

95 papers A* 12A 4B 13Journal 39Unranked 20

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