%%% ====================================================================
%%% BibTeX-file{
%%% author = "Andrew M. Pitts",
%%% date = "2009-04-15",
%%% filename = "PittsAM.bib",
%%% url = "http://www.cl.cam.ac.uk/users/amp12/bib/PittsAM.bib",
%%% www-home = "http://www.cl.cam.ac.uk/users/amp12/",
%%% address = "Cambridge University Computer Laboratory,
%%% JJ Thomson Avenue, Cambridge CB3 0FD, UK",
%%% email = "amp12 at cl.cam.ac.uk",
%%% telephone = "+44 223 334629",
%%% FAX = "+44 223 334678",
%%% dates = {1980--},
%%% keywords = "",
%%% FTP-archive = ,
%%% supported = "yes",
%%% supported-by = "Andrew Pitts",
%%% abstract = "Bibliography for Andrew M. Pitts"
%%% }
%%% ====================================================================
@ARTICLE{PittsAM:trit,
AUTHOR = {J.~M.~E.~Hyland and P.~T.~Johnstone and A.~M.~Pitts},
TITLE = {Tripos Theory},
JOURNAL = {Math.\ Proc.\ Cambridge Philos.\ Soc.},
VOLUME = 88,
YEAR = 1980,
PAGES = {205--232}
}
@PHDTHESIS{PittsAM:thet,
AUTHOR = {A.~M.~Pitts},
TITLE = {The Theory of Triposes},
SCHOOL = {University of Cambridgexs},
YEAR = 1981
}
@ARTICLE{PittsAM:fuzsdn,
AUTHOR = {A.~M.~Pitts},
TITLE = {Fuzzy Sets Do Not Form a Topos (Short
Communication)},
JOURNAL = {Fuzzy Sets and Systems},
VOLUME = 8,
YEAR = 1982,
PAGES = {101--104}
}
@ARTICLE{PittsAM:amaich,
AUTHOR = {A.~M.~Pitts},
TITLE = {Amalgamation and Interpolation in the Category of
{Heyting} Algebras},
JOURNAL = {Jour.\ Pure and Appl.\ Algebra},
VOLUME = 29,
YEAR = 1983,
PAGES = {155--165}
}
@ARTICLE{PittsAM:appomc,
AUTHOR = {A.~M.~Pitts},
TITLE = {An Application of Open Maps to Categorical Logic},
JOURNAL = {Jour. Pure and Appl. Algebra},
VOLUME = 29,
YEAR = 1983,
PAGES = {313--326}
}
@ARTICLE{PittsAM:procbt,
AUTHOR = {A.~M.~Pitts},
TITLE = {On Product and Change of Base for Toposes},
JOURNAL = {Cahier de Top.\ et G{\'e}om.\ Diff.},
VOLUME = 26,
YEAR = 1985,
PAGES = {43--61}
}
@INCOLLECTION{PittsAM:intccp,
AUTHOR = {A.~M.~Pitts},
TITLE = {Interpolation and Conceptual Completeness for
Pretoposes Via Category Theory},
BOOKTITLE = {Mathematical Logic and Theoretical Computer Science},
PUBLISHER = {Marcel Dekker Inc., New York},
YEAR = 1987,
PAGES = {301--327}
}
@ARTICLE{PittsAM:reslfp,
AUTHOR = {M.~Makkai and A.~M.~Pitts},
TITLE = {Some Results on Locally Finitely Presentable
Categories},
JOURNAL = {Trans.\ Amer.\ Math.\ Soc.},
VOLUME = 299,
YEAR = 1987,
PAGES = {473--496}
}
@INPROCEEDINGS{PittsAM:polist,
AUTHOR = {A.~M.~Pitts},
TITLE = {Polymorphism Is Set Theoretic, Constructively},
BOOKTITLE = {Category Theory and Computer Science, Proc.\
Edinburgh 1987},
EDITOR = {D.~H.~Pitt and A.~Poign{\'e} and D.~E.~Rydeheard},
SERIES = {Lecture Notes in Computer Science},
PUBLISHER = {Springer-Verlag, Berlin},
VOLUME = 283,
YEAR = 1987,
PAGES = {12--39}
}
@ARTICLE{PittsAM:revls,
AUTHOR = {A.~M.~Pitts},
TITLE = {Review of: {J.} {Lambek} and {P.} {J.} {Scott},
{Introduction} to Higher Order Categorical Logic},
JOURNAL = {Bull.\ London Math.\ Soc.},
VOLUME = 19,
YEAR = 1987,
PAGES = {190--192}
}
@ARTICLE{PittsAM:appsec,
AUTHOR = {A.~M.~Pitts},
TITLE = {Applications of Sup-lattice Enriched Category Theory
to Sheaf Theory},
JOURNAL = {Proc.\ London Math.\ Soc.},
VOLUME = 57,
YEAR = 1988,
PAGES = {433--480}
}
@ARTICLE{PittsAM:concfo,
AUTHOR = {A.~M.~Pitts},
TITLE = {Conceptual Completeness for First Order
Intuitionistic Logic: an Application of Categorical
Logic},
JOURNAL = {Annals Pure Applied Logic},
VOLUME = 41,
YEAR = 1989,
PAGES = {33--81}
}
@INPROCEEDINGS{PittsAM:theccs,
AUTHOR = {J.~M.~E.~Hyland and A.~M.~Pitts},
TITLE = {The Theory of Constructions: Categorical Semantics
and Topos-theoretic Models},
BOOKTITLE = {Categories in Computer Science and Logic},
EDITOR = {J.~W.~Gray and A.~Scedrov},
SERIES = {Contemporary Mathematics},
PUBLISHER = {Amer.\ Math.\ Soc, Providence RI},
VOLUME = 92,
YEAR = 1989,
PAGES = {137-199}
}
@INPROCEEDINGS{PittsAM:nontpt,
AUTHOR = {A.~M.~Pitts},
TITLE = {Non-trivial Power Types Can't Be Subtypes of
Polymorphic Types},
BOOKTITLE = {4th Annual Symposium on Logic in Computer Science},
PUBLISHER = {IEEE Computer Society Press, Washington},
YEAR = 1989,
PAGES = {6--13}
}
@ARTICLE{PittsAM:notrpl,
AUTHOR = {A.~M.~Pitts and P.~Taylor},
TITLE = {A Note on {Russell's} {Paradox} in Locally Cartesian
Closed Categories},
JOURNAL = {Studia Logica},
VOLUME = 48,
YEAR = 1989,
PAGES = {377--387}
}
@PROCEEDINGS{PittsAM:ctcs89,
EDITOR = {P.~Dybjer and D.~H.~Pitt and A.~M.~Pitts and
A.~Poign{\'e} and D.~E.~Rydeheard},
TITLE = {Category Theory and Computer Science, Proceedings
{Manchester}, UK, 1989},
PUBLISHER = {Springer-Verlag, Berlin},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 389,
YEAR = 1989
}
@UNPUBLISHED{PittsAM:notcl,
AUTHOR = {A.~M.~Pitts},
TITLE = {Notes on Categorical Logic},
NOTE = {Lecture Notes for a graduate course in the
University of Cambridge Computer Laboratory, 78pp
typescript},
MONTH = {Lent Term},
YEAR = 1989
}
@INPROCEEDINGS{PittsAM:nffc,
AUTHOR = {R.~L.~Crole and A.~M.~Pitts},
TITLE = {New Foundations for Fixpoint Computations},
BOOKTITLE = {5th Annual Symposium on Logic in Computer Science},
PUBLISHER = {IEEE Computer Society Press, Washington},
YEAR = 1990,
PAGES = {489--497},
NOTE = {(see \cite{PittsAM:newffcff} for an expanded and
revised version of this extended abstract)}
}
@ARTICLE{PittsAM:repctc,
AUTHOR = {A.~M.~Pitts},
TITLE = {Report on the Category Theory and Computer Science
Conference, {Manchester} {U}{K}, {September} 1989},
JOURNAL = {Bulletin of the EATCS},
VOLUME = 41,
YEAR = 1990,
PAGES = {268--270}
}
@INPROCEEDINGS{PittsAM:evall,
AUTHOR = {A.~M.~Pitts},
TITLE = {Evaluation Logic},
BOOKTITLE = {IVth Higher Order Workshop, {Banff} 1990},
SERIES = {Workshops in Computing},
EDITOR = {G.~Birtwistle},
PUBLISHER = {Springer-Verlag, Berlin},
YEAR = 1991,
PAGES = {162--189},
ABSTRACT = {A new typed, higher-order logic is described which
appears particularly well fitted to reasoning about
forms of computation whose operational behaviour can
be specified using the {\em Natural Semantics\/}
style of structural operational
semantics~\cite{Kah}. The logic's underlying type
system is Moggi's {\em computational
metalanguage}~\cite{Mog1}, which enforces a
distinction between computations and values via the
categorical structure of a strong monad. This is
extended to a (constructive) predicate logic with
modal formulas about evaluation of computations to
values, called {\em evaluation modalities}. The
categorical structure corresponding to this kind of
logic is explained and a couple of examples of
categorical models given.\par As a first example of
the naturalness and applicability of this new logic
to program semantics, we investigate the translation
of a (tiny) fragment of Standard ML into a theory
over the logic, which is proved computationally
adequate for ML's Natural Semantics~\cite{MTH}.
Whilst it is tiny, the ML fragment does however
contain both higher-order functional and imperative
features, about which the logic allows us to reason
without having to mention global states explicitly.}
}
@PROCEEDINGS{PittsAM:ctcs91,
EDITOR = {S.~Abramsky and {P.-L.} Curien and D.~H.~Pitt and
A.~M.~Pitts and A.~Poign{\'e} and D.~E.~Rydeheard},
TITLE = {Category Theory and Computer Science, Proceedings,
{Paris}, {France},1991},
PUBLISHER = {Springer-Verlag, Berlin},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 530,
YEAR = 1991
}
@ARTICLE{PittsAM:revbw,
AUTHOR = {A.~M.~Pitts},
TITLE = {Review of: {M.} {Barr} and {C.} {Wells}, {Toposes},
Triples and Theories},
JOURNAL = {Jour.\ Symbolic Logic},
VOLUME = 56,
YEAR = 1991,
PAGES = {340--341}
}
@ARTICLE{PittsAM:repsac,
AUTHOR = {A.~M.~Pitts},
TITLE = {Report on the Symposium on Applications of
Categories in Computer Science, {Durham} {U}{K},
{July} 1991},
JOURNAL = {London Mathematical Society Newsletter},
VOLUME = 189,
YEAR = 1991
}
@ARTICLE{PittsAM:newffcff,
AUTHOR = {R.~L.~Crole and A.~M.~Pitts},
TITLE = {New Foundations for Fixpoint Computations:
FIX-hyperdoctrines and the FIX-logic},
JOURNAL = {Information and Computation},
VOLUME = 98,
YEAR = 1992,
PAGES = {171--210}
}
@ARTICLE{PittsAM:intsoq,
AUTHOR = {A.~M.~Pitts},
TITLE = {On an Interpretation of Second Order Quantification
in First Order Intuitionistic Propositional Logic},
JOURNAL = {Jour.\ Symbolic Logic},
VOLUME = 57,
YEAR = 1992,
PAGES = {33--52},
ABSTRACT = {We prove the following surprising property of
Heyting's intuitionistic propositional calculus,
$\IpC$. Consider the collection of formulas, $\phi$,
built up from propositional variables
($p,q,r,\ldots$) and falsity ($\F$) using
conjunction ($\conj$), disjunction ($\disj$) and
implication ($\imp$). Write $\vdash\phi$ to indicate
that such a formula is intuitionistically valid. We
show that for each variable $p$ and formula $\phi$
there exists a formula $\All_p\phi$ (effectively
computable from $\phi$), containing only variables
not equal to $p$ which occur in $\phi$, and such
that for all formulas $\psi$ not involving $p$,
$\vdash\psi\imp\All_p\phi$ if and only if
$\vdash\psi\imp\phi$. Consequently quantification
over propositional variables can be modelled in
$\IpC$, and there is an interpretation of the second
order propositional calculus, $\IpC^2$, in $\IpC$
which restricts to the identity on first order
propositions.\par An immediate corollary is the
strengthening of the usual Interpolation Theorem for
$\IpC$ to the statement that there are least and
greatest interpolant formulas for any given pair of
formulas. The result also has a number of
interesting consequences for the algebraic
counterpart of $\IpC$, the theory of Heyting
algebras. In particular we show that a model of
$\IpC^2$ can be constructed whose algebra of
truth-values is equal to any given Heyting algebra.}
}
@BOOK{PittsAM:appccs,
EDITOR = {M.~P.~Fourman and P.~T.~Johnstone and A.~M.~Pitts},
TITLE = {Applications of Categories in Computer Science,
Proceedings {L}{M}{S} {Symposium}, {Durham}, {U}{K},
1991},
PUBLISHER = {Cambridge University Press},
SERIES = {LMS Lecture Note Series},
VOLUME = 177,
YEAR = 1992
}
@INPROCEEDINGS{PittsAM:relprd,
AUTHOR = {A.~M.~Pitts},
TITLE = {Relational Properties of Recursively Defined
Domains},
BOOKTITLE = {8th Annual Symposium on Logic in Computer Science},
PUBLISHER = {IEEE Computer Society Press, Washington},
YEAR = 1993,
PAGES = {86--97}
}
@INPROCEEDINGS{PittsAM:bisct,
AUTHOR = {A.~M.~Pitts},
TITLE = {Bisimulation and Co-induction ({Tutorial}) },
BOOKTITLE = {8th Annual Symposium on Logic in Computer Science},
PUBLISHER = {IEEE Computer Society Press, Washington},
YEAR = 1993,
PAGES = {2--3},
ABSTRACT = {The use of positive inductive definitions pervades
the mathematical and logical foundations of computer
science. The dual concept of co-inductive (or
negative inductive) definition is also important, if
somewhat less common. It often arises when
constructing and reasoning about (potentially)
infinite objects. In this tutorial talk I will
concentrate on co-inductively defined equality
relations and the use of `bisimulations' to
establish equalitites. The talk will describe the
origin of this technique in the theory of concurrent
processes, will touch upon its general formulation,
and will dwell upon recent applications of it for
reasoning about equality of functional programs,
both from an operational and a denotational point of
view. [Note: This abstract did not appear in the
original conference paper; it was supplied by the
author for this bibliography.]}
}
@INPROCEEDINGS{PittsAM:obspho,
AUTHOR = {A.~M.~Pitts and I.~D.~B.~Stark},
TITLE = {On the Observable Properties of Higher Order
Functions That Dynamically Create Local Names
(Preliminary Report)},
BOOKTITLE = {Workshop on State in Programming Languages,
{Copenhagen}, 1993},
ORGANIZATION = {ACM SIGPLAN},
NOTE = {Yale Univ.\ Dept.\ Computer Science Technical Report
YALEU/DCS/RR-968},
YEAR = 1993,
PAGES = {31--45},
ABSTRACT = {The research reported in this paper is concerned
with the problem of reasoning about properties of
higher order functions involving state. It is
motivated by the desire to identify what, if any,
are the difficulties created purely by {\em
locality\/} of state, independent of other
properties such as side-effects, exceptional
termination and non-termination due to recursion. We
consider a simple language (equivalent to a fragment
of Standard ML) of typed, higher order functions
that can dynamically create fresh {\em names}. Names
are created with local scope, can be tested for
equality and can be passed around via function
application, but that is all.\par We demonstrate
that despite the simplicity of the language and its
operational semantics, the observable properties of
such functions can be very subtle. Two methods are
introduced for analyzing Morris-style observational
equivalence between expressions in the language. The
first method introduces a notion of `applicative'
equivalence incorporating a syntactic version of
O'Hearn and Tennent's relationally parametric
functors and a version of {\em representation
independence\/} for local names. This applicative
equivalence is properly contained in the relation of
observational equivalence, but coincides with it for
first order expressions (and is decidable
there). The second method develops a general,
categorical framework for computationally adequate
models of the language, based on Moggi's {\em
monadic\/} approach to denotational semantics. We
give examples of models, one of which is fully
abstract for first order expressions. No fully
abstract (concrete) model of the whole language is
known.}
}
@INPROCEEDINGS{PittsAM:obsphown,
AUTHOR = {A.~M.~Pitts and I.~D.~B.~Stark},
TITLE = {Observable Properties of Higher Order Functions That
Dynamically Create Local Names, or: What's new?},
BOOKTITLE = {Mathematical Foundations of Computer Science, Proc.\
18th Int.\ Symp., {Gda{\'n}sk}, 1993},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 711,
PUBLISHER = {Springer-Verlag, Berlin},
YEAR = 1993,
PAGES = {122--141},
ABSTRACT = {The research reported in this paper is concerned
with the problem of reasoning about properties of
higher order functions involving state. It is
motivated by the desire to identify what, if any,
are the difficulties created purely by {\em
locality\/} of state, independent of other
properties such as side-effects, exceptional
termination and non-termination due to recursion. We
consider a simple language (equivalent to a fragment
of Standard ML) of typed, higher order functions
that can dynamically create fresh {\em names\/};
names are created with local scope, can be tested
for equality and can be passed around via function
application, but that is all. Despite the extreme
simplicity of the language and its operational
semantics, the observable properties of such
functions are shown to be very subtle. A notion of
`logical relation' is introduced which incorporates
a version of {\em representation independence\/} for
local names. We show how to use it to establish
observational equivalences. The method is shown to
be complete (and decidable) for expressions of first
order types, but incomplete at higher types.}
}
@INCOLLECTION{PittsAM:hl,
AUTHOR = {M.~J.~C.~Gordon and A.~M.~Pitts},
TITLE = {The {H}{O}{L} {L}ogic},
BOOKTITLE = {Introduction to {H}{O}{L}, Part III},
EDITOR = {M.~J.~C.~Gordon and T.~F.~Melham},
PUBLISHER = {Cambridge University Press},
YEAR = 1993,
PAGES = {191-232}
}
@TECHREPORT{PittsAM:intbct,
AUTHOR = {J.~W.~Gray and A.~M.~Pitts and K.~Seiber},
TITLE = {Interactions Between Category Theory and Computer
Science, {19.07.--23.07.93} (9329)},
NUMBER = {Dagstuhl-Seminar-Report 69},
INSTITUTION = {Internationales Begegnungs und Forschungszentrum
Schloss Dagstuhl, Germany},
YEAR = 1993
}
@ARTICLE{PittsAM:coiprd,
AUTHOR = {A.~M.~Pitts},
TITLE = {A Co-induction Principle for Recursively Defined
Domains},
JOURNAL = {Theoretical Computer Science},
VOLUME = 124,
YEAR = 1994,
PAGES = {195--219},
NOTE = {(A preliminary version of this work appeared as
Cambridge Univ. Computer Laboratory
Tech. Rept. No.~252, April 1992.)},
ABSTRACT = {This paper establishes a new property of predomains
recursively defined using the cartesian product,
disjoint union, partial function space and convex
powerdomain constructors. We prove that the partial
order on such a recursive predomain $D$ is the
greatest fixed point of a certain monotone operator
associated to $D$. This provides a structurally
defined family of proof principles for these
recursive predomains: to show that one element of
$D$ approximates another, it suffices to find a
binary relation containing the two elements that is
a post-fixed point for the associated monotone
operator. The statement of the proof principles is
independent of any of the various methods available
for explicit construction of recursive
predomains. Following Milner and Tofte, the method
of proof is called {\em co-induction}. It closely
resembles the way bisimulations are used in
concurrent process calculi.\par Two specific
instances of the co-induction principle already
occur in work of Abramsky in the form of `internal
full abstraction' theorems for denotational
semantics of SCCS and the lazy lambda calculus. In
the first case post-fixed binary relations are
precisely Abramsky's {\em partial bisimulations},
whereas in the second case they are his {\em
applicative bisimulations}. The co-induction
principle also provides an apparently useful tool
for reasoning about equality of elements of
recursively defined datatypes in (strict or lazy)
higher order functional programming languages.}
}
@INPROCEEDINGS{PittsAM:compavm,
AUTHOR = {A.~M.~Pitts},
TITLE = {Computational Adequacy via `Mixed' Inductive
Definitions},
BOOKTITLE = {Mathematical Foundations of Programming Semantics,
Proc.\ 9th Int.\ Conf., {New} {Orleans}, LA, USA,
April 1993},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 802,
PUBLISHER = {Springer-Verlag, Berlin},
YEAR = 1994,
PAGES = {72--82},
ABSTRACT = {For programming languages whose denotational
semantics uses fixed points of domain constructors
of mixed variance, proofs of correspondence between
operational and denotational semantics (or between
two different denotational semantics) often depend
upon the existence of relations specified as the
fixed point of non-monotonic operators. This paper
describes a new approach to constructing such
relations which avoids having to delve into the
detailed construction of the recursively defined
domains themselves. The method is introduced by
example, by considering the proof of computational
adequacy of a denotational semantics for expression
evaluation in a simple, untyped functional
programming language.}
}
@INCOLLECTION{PittsAM:hls,
AUTHOR = {M.~J.~C.~Gordon and A.~M.~Pitts},
TITLE = {The {H}{O}{L} Logic and System},
BOOKTITLE = {Towards Verified Systems},
CHAPTER = 3,
EDITOR = {J.~Bowen},
SERIES = {Real-Time Safety Critical Systems},
VOLUME = 2,
PUBLISHER = {Elsevier Science {B.V.}},
YEAR = 1994,
PAGES = {49-70}
}
@INPROCEEDINGS{PittsAM:fulatb,
AUTHOR = {E.~Ritter and A.~M.~Pitts},
TITLE = {A Fully Abstract Translation between a
$\lambda$-Calculus with Reference Types and
{Standard} {M}{L}},
BOOKTITLE = {2nd Int. Conf. on Typed Lambda Calculus and
Applications, Edinburgh, 1995},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 902,
PUBLISHER = {Springer-Verlag, Berlin},
YEAR = 1995,
PAGES = {397--413},
ABSTRACT = {This paper describes a syntactic translation for a
substantial fragment of the core Standard ML
language into a typed lambda calculus with recursive
types and imperative features in the form of
reference types. The translation compiles SML's use
of declarations and pattern matching into lambda
terms, and transforms the use of environments in the
operational semantics into a simpler relation of
evaluation to canonical form. The translation is
shown to be `fully abstract', in the sense that it
both preserves and reflects observational
equivalence (also commonly called contextual
equivalence). A co-inductively defined notion of
applicative bisimilarity for lambda calculi with
state is developed to establish this result.}
}
@TECHREPORT{PittsAM:somnic,
AUTHOR = {A. M. Pitts},
TITLE = {Some Notes on Inductive and Co-Inductive Techniques
in the Semantics of Functional Programs},
INSTITUTION = {{BRICS}},
YEAR = 1994,
TYPE = {Notes Series},
NUMBER = {BRICS-NS-94-5},
ADDRESS = {Department of Computer Science, University of
Aarhus},
MONTH = dec,
NOTE = {vi+135 pp, draft version},
ABSTRACT = {These notes were handed out at a course on {\em
Inductive and Co-Inductive Techniques in the
Semantics of Functional Programs} given by Andrew
Pitts, The Computer Laboratory, Cambridge
University, while visiting BRICS 21 November -- 2
December 1994. The course material included these
notes, the report {\em Relational Properties of
Domains} and slides.\\[.5ex] {\bf Course
Description}\\ The aim of the course is to describe
recent advances in formal techniques for
establishing observational equivalence of functional
programs. It considers both operational and
denotational methods and the relationship between
them. One goal is to give an exposition of Howe's
method for characterizing observational equivalence
as a co-inductively defined ``applicative
bisimulation''. Another goal is to describe Freyd's
analysis of recursively defined domains in terms of
a property of mixed
initiality/finality. Applications of this are given
to proving correspondence of operational and
denotational semantics and to inductive and
co-inductive reasoning about ``user-declared''
datatypes.}
}
@ARTICLE{PittsAM:revmm,
AUTHOR = {A.~M.~Pitts},
TITLE = {Review of: {S}.~{Mac}~{Lane} and {I.}~{Moerdijk},
{Sheaves} in geometry and logic. A first
introduction to topos theory},
JOURNAL = {Journ.\ Symbolic Logic},
VOLUME = 60,
YEAR = 1995,
PAGES = {340--342}
}
@InCollection{PittsAM:catl,
author = {A. M. Pitts},
title = {Categorical Logic},
booktitle = {Handbook of Logic in Computer Science, Volume
5. Algebraic and Logical Structures},
publisher = {Oxford University Press},
year = 2000,
pages = {39--128},
editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
isbn = {0-19-853781-6},
url = {http://www.oup.co.uk/isbn/0-19-853781-6}
}
@Comment TECHREPORT{PittsAM:catl,
@Comment AUTHOR={A.~M.~Pitts},
@Comment TITLE={Categorical Logic},
@Comment INSTITUTION={University of Cambridge Computer Laboratory},
@Comment YEAR=1995,
@Comment TYPE={Technical Report},
@Comment NUMBER=367,
@Comment MONTH=may,
@Comment NOTE={94 pages},
@Comment ABSTRACT={This document provides an introduction to the interaction
@Comment between category theory and mathematical logic which is slanted
@Comment towards computer scientists.}}
@ARTICLE{PittsAM:relpod,
AUTHOR = {A.~M.~Pitts},
TITLE = {Relational Properties of Domains},
JOURNAL = {Information and Computation},
VOLUME = 127,
YEAR = 1996,
PAGES = {66--90},
NOTE = {(A preliminary version of this work appeared as
Cambridge Univ. Computer Laboratory
Tech. Rept. No.~321, December 1993.)},
ABSTRACT = {New tools are presented for reasoning about
properties of recursively defined domains. We work
within a general, category-theoretic framework for
various notions of `relation' on domains and for
actions of domain constructors on relations.
Freyd's analysis of recursive types in terms of a
property of mixed initiality/finality is transferred
to a corresponding property of {\em invariant\/}
relations. The existence of invariant relations is
proved under completeness assumptions about the
notion of relation. We show how this leads to
simpler proofs of the computational adequacy of
denotational semantics for functional programming
languages with user-declared datatypes. We show how
the initiality/finality property of invariant
relations can be specialized to yield an induction
principle for admissible subsets of recursively
defined domains, generalizing the principle of
structural induction for inductively defined
sets. We also show how the initiality/finality
property gives rise to the co-induction principle
studied by the author ({\em Theoretical Computer
Science\/} {\bf 124}, 195--219 (1994)), by which
equalities between elements of recursively defined
domains may be proved via an appropriate notion of
`bisimulation'.}
}
@INCOLLECTION{PittsAM:opebtp,
AUTHOR = {A.~M.~Pitts},
TITLE = {Operationally-Based Theories of Program Equivalence},
BOOKTITLE = {Semantics and Logics of Computation},
EDITOR = {P.~Dybjer and A.~M.~Pitts},
PUBLISHER = {Cambridge University Press},
SERIES = {Publications of the Newton Institute},
YEAR = 1997,
PAGES = {241--298},
ABSTRACT = {The aim of these notes is to describe some recent
advances in verification techniques based on
operational semantics. We focus upon properties of
contextual equivalence (and of contextual
preordering) of expressions in a simple, non-strict
functional programming language equipped with an
inductively defined notion of evaluation to
canonical form. The co-inductive characterisation
of contextual equivalence in terms of bisimulations
is presented. The use of co-induction for reasoning
about recursively defined elements of lazy datatypes
is illustrated. We give operationally-based proofs
of the rational completeness and syntactic
continuity properties of the contextual preorder.}
}
@Comment INPROCEEDINGS{PittsAM:realvo1,
@Comment AUTHOR={A.~M.~Pitts},
@Comment TITLE={Reasoning About Local Variables with Operationally-Based
@Comment Logical Relations},
@Comment BOOKTITLE={11th Annual Symposium on Logic in Computer Science},
@Comment PUBLISHER={IEEE Computer Society Press, Washington},
@Comment YEAR=1996,
@Comment PAGES={152--163},
@Comment}
@Comment INPROCEEDINGS{PittsAM:procbe1,
@Comment AUTHOR={A.~M.~Pitts and J.~R.~X.~Ross},
@Comment TITLE={Process Calculus Based Upon Evaluation to Committed Form},
@Comment BOOKTITLE={CONCUR'96: Concurrency Theory, Proc.\ 7th Int.\ Conf.\,
@Comment Pisa, 1996.},
@Comment EDITOR={U.~Montanari and V.~Sassone},
@Comment SERIES={Lecture Notes in Computer Science},
@Comment VOLUME=1119,
@Comment PUBLISHER={Springer-Verlag, Berlin},
@Comment YEAR=1996,
@Comment PAGES={18--33},
@Comment ABSTRACT={An approach to the semantics of CCS-like communicating
@Comment processes is proposed that is based upon evaluation of processes
@Comment to input- or output-committed form, with no explicit mention of
@Comment silent actions. This leads to a co-inductively defined notion of
@Comment \emph{evaluation bisimilarity}---a form of weak equivalence which
@Comment is shown to be a congruence, even in the presence of summation.
@Comment The relationship between this evaluation-based approach and the
@Comment more traditional, labelled transition semantics is investigated.
@Comment In particular, with some restriction on sums, CCS observation
@Comment equivalence is characterised purely in terms of evaluation to
@Comment committed form, and evaluation bisimilarity is characterised as a
@Comment weak delay equivalence. These results are extended to the higher
@Comment order case, where evaluation bisimilarity coincides with
@Comment Sangiorgi's weak context bisimilarity. An evaluation-based
@Comment approach to $\pi$-calculus and the relationship with Milner and
@Comment Sangiorgi's reduction-based notion of barbed bisimulation are
@Comment also examined.}
@Comment}
@ARTICLE{PittsAM:notlrb,
AUTHOR = {A.~M.~Pitts},
TITLE = {A Note on Logical Relations Between Semantics and
Syntax},
JOURNAL = {Logic Journal of the Interest Group in Pure and
Applied Logics},
VOLUME = 5,
NUMBER = 4,
MONTH = jul,
PAGES = {589--601},
YEAR = 1997,
ABSTRACT = {This note gives a new proof of the `operational
extensionality' property of Abramsky's lazy lambda
calculus--namely the coincidence of contextual
equivalence with a co-inductively defined notion of
`applicative bisimilarity'. This purely syntactic
result is here proved using a logical relation (due
to Plotkin) between the syntax and its denotational
semantics. The proof exploits a mixed
inductive/co-inductive characterisation of the
logical relation recently discovered by the author.
(Full version of an invited paper presented at the
{\em 3rd Workshop on Logic, Language, Information
and Computation\/} ({\em WoLLIC'96\/}), May 8--10,
Salvador (Bahia), Brazil, organised by UFPE and
UFBA, sponsored by IGPL, FoLLI, and ASL.)}
}
@INCOLLECTION{PittsAM:realvo,
AUTHOR = {A.~M.~Pitts},
TITLE = {Reasoning About Local Variables with
Operationally-Based Logical Relations},
BOOKTITLE = {Algol-Like Languages},
EDITOR = {P.~W.~O'Hearn and R.~D.~Tennent},
VOLUME = 2,
CHAPTER = 17,
PUBLISHER = {Birkhauser},
YEAR = 1997,
PAGES = {173--193},
NOTE = {Reprinted from \emph{Proceedings Eleventh Annual
IEEE Symposium on Logic in Computer Science},
Brunswick, NJ, July 1996, pp~152--163.},
ABSTRACT = {A parametric logical relation between the phrases of
an Algol-like language is presented. Its definition
involves the structural operational semantics of the
language, but was inspired by recent
denotationally-based work of O'Hearn and Reynolds on
translating Algol into a predicatively polymorphic
linear lambda calculus. The logical relation yields
an applicative characterisation of contextual
equivalence for the language and provides a useful
(and complete) method for proving equivalences. Its
utility is illustrated by giving simple and direct
proofs of some contextual equivalences, including an
interesting equivalence due to O'Hearn which hinges
upon the undefinability of `snapback' operations
(and which goes beyond the standard suite of
`Meyer-Sieber' examples). Whilst some of the
mathematical intricacies of denotational semantics
are avoided, the hard work in this operational
approach lies in establishing the `fundamental
property' for the logical relation---the proof of
which makes use of a compactness property of
fixpoint recursion with respect to evaluation of
phrases. But once this property has been
established, the logical relation provides a
verification method with an attractively low
mathematical overhead.}
}
@BOOK{PittsAM:semlc,
EDITOR = {A.~M.~Pitts and P.~Dybjer},
TITLE = {Semantics and Logics of Computation},
PUBLISHER = {Cambridge University Press},
SERIES = {Publications of the Newton Institute},
ISBN = {0-521-58057-9},
YEAR = 1997
}
@ARTICLE{PittsAM:procbu,
AUTHOR = {A.~M.~Pitts and J.~R.~X.~Ross},
TITLE = {Process Calculus Based Upon Evaluation to Committed
Form},
JOURNAL = {Theoretical Computer Science},
VOLUME = 195,
YEAR = 1998,
PAGES = {155--182},
NOTE = {A preliminary version of this paper appeared in
CONCUR'96, Lecture Notes in Computer Science
Vol.~1119 (Springer-Verlag, Berlin, 1996),
pp~18--33},
ABSRACT = {An approach to the semantics of CCS-like
communicating processes is proposed that is based
upon evaluation of processes to input- or
output-committed form, with no explicit mention of
silent actions. This leads to a co-inductively
defined notion of evaluation bisimilarity---a form
of weak branching-time equivalence which is shown to
be a congruence, even in the presence of summation.
The relationship between this evaluation-based
approach and the more traditional, labelled
transition semantics is investigated. In
particular, with some restriction on sums, CCS
observation equivalence is characterised purely in
terms of evaluation to committed form, and
evaluation bisimilarity is characterised as a weak
delay equivalence. These results are extended to
the higher order case, where evaluation bisimilarity
coincides with Sangiorgi's weak context
bisimilarity. An evaluation-based approach to
pi-calculus and the relationship with Milner and
Sangiorgi's reduction-based notion of barbed
bisimulation are also examined.}
}
@INCOLLECTION{PittsAM:operfl,
AUTHOR = {A.~M.~Pitts and I.~D.~B.~Stark},
TITLE = {Operational Reasoning for Functions with Local
State},
BOOKTITLE = {Higher Order Operational Techniques in Semantics},
EDITOR = {A.~D.~Gordon and A.~M.~Pitts},
YEAR = 1998,
PUBLISHER = {Cambridge University Press},
SERIES = {Publications of the Newton Institute},
PAGES = {227--273},
ABSRACT = {Languages such as ML or Lisp permit the use of
recursively defined function expressions with
locally declared storage locations. Although this
can be very convenient from a programming point of
view it severely complicates the properties of
program equivalence even for relatively simple
fragments of such languages---such as the simply
typed fragment of Standard~ML with integer-valued
references considered here. This paper presents a
method for reasoning about \emph{contextual
equivalence} of programs involving this combination
of functional and procedural features. The method is
based upon the use of a certain kind of
\emph{logical relation} parameterised by relations
between program states. The form of this logical
relation is novel, in as much as it involves
relations not only between program expressions, but
also between program continuations (also known as
\emph{evaluation contexts}). The authors found this
approach necessary in order to establish the
`Fundamental Property of logical relations' in the
presence of both dynamically allocated local state
and recursion. The logical relation characterises
contextual equivalence and yields a proof of the
best known context lemma for this kind of
language---the Mason-Talcott \Quote{ciu} theorem.
Moreover, it is shown that the method can prove
examples where such a context lemma is not much help
and which involve representation independence,
higher order memoising functions, and profiling
functions.}
}
@book{GordonAD:higoot,
editor = {A.~D. Gordon and A.~M. Pitts},
title = {Higher Order Operational Techniques in Semantics},
publisher = {Cambridge University Press},
series = {Publications of the Newton Institute},
year = 1998,
isbn = {0-521-63168-8}
}
@inproceedings{PittsAM:exitlr,
author = {A.~M.~Pitts},
title = {Existential Types: Logical Relations and Operational
Equivalence},
booktitle = {Automata, Languages and Programming, 25th
International Colloquium, ICALP'98, Aalborg,
Denmark, July 1998, Proceedings},
editor = {K.~G.~Larsen and S.~Skyum and G.~Winskel},
series = {Lecture Notes in Computer Science},
volume = 1443,
publisher = {Springer-Verlag, Berlin},
year = 1998,
pages = {309--326},
abstract = {Existential types have proved useful for classifying
various kinds of information hiding in programming
languages, such as occurs in abstract datatypes and
objects. In this paper we address the question of
when two elements of an existential type are
semantically equivalent. Of course, it depends what
one means by `semantic equivalence'. Here we take a
syntactic approach---so semantic equivalence will
mean some kind of operational equivalence. The paper
begins by surveying some of the literature on this
topic involving `logical relations'. Matters become
quite complicated if the programming language mixes
existential types with function types and features
involving non-termination (such as recursive
definitions). We give an example (suggested by
Ian~Stark) to show that in this case the existence
of suitable relations is sufficient, but not
necessary for proving operational equivalences at
existential types. Properties of this and other
examples are proved using a new form of
operationally-based logical relation which does in
fact provide a useful characterisation of
operational equivalence for existential types.}
}
@Proceedings{PittsAM:secwho,
title = {Second Workshop on Higher-Order Operational
Techniques in Semantics (HOOTS II), Stanford
University, December 8-12, 1997},
year = 1998,
editor = {A.~D.~Gordon and A.~M.~Pitts and C.~Talcott},
volume = 10,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier}
}
@InProceedings{PittsAM:opevdm,
author = {A.~M.~Pitts},
title = {Operational Versus Denotational Methods in the
Semantics of Higher Order Languages (Tutorial)},
booktitle = {Principles of Declarative Programming, 10th Int.\
Symp., PLILP'98},
editor = {C.~Palamidessi and H.~Glaser and K.~Meinke},
volume = 1490,
series = {Lecture Notes in Computer Science},
year = 1998,
publisher = {Springer-Verlag, Berlin},
pages = {282--283},
}
@Article{PittsAM:parpoe,
author = {A.~M.~Pitts},
title = {Parametric Polymorphism and Operational Equivalence},
journal = {Mathematical Structures in Computer Science},
year = 2000,
volume = 10,
pages = {321--359},
issn = {0960-1295},
note = {A preliminary version appeared in \emph{Proceedings,
Second Workshop on Higher Order Operational
Techniques in Semantics (HOOTS II), Stanford CA,
December 1997}, Electronic Notes in Theoretical
Computer Science 10, 1998.}
}
@Comment TechReport{PittsAM:parpoe-tr,
@Comment author = {A.~M.~Pitts},
@Comment title = {Parametric Polymorphism and Operational Equivalence},
@Comment institution = {Cambridge University Computer Laboratory},
@Comment year = 1998,
@Comment number = 453,
@Comment abstract = {Studies of the mathematical properties of
@Comment impredicative polymorphic types have for the most part focused on
@Comment the \emph{polymorphic lambda calculus} of Girard-Reynolds, which is
@Comment a calculus of \emph{total} polymorphic functions. This paper
@Comment considers polymorphic types from a functional programming
@Comment perspective, where the partialness arising from the presence of
@Comment fixpoint recursion complicates the nature of potentially infinite
@Comment (`lazy') datatypes. An approach to Reynolds' notion of
@Comment \emph{relational parametricity} is developed that works directly on
@Comment the syntax of a programming language, using a novel closure operator
@Comment to relate operational behaviour to parametricity properties of
@Comment types. Working with an extension of Plotkin's PCF with
@Comment $\forall$-types, lazy lists and existential types, we show by
@Comment example how the resulting logical relation can be used to prove
@Comment properties of polymorphic types up to operational equivalence.},
@Comment note = {A preliminary version appeared in \emph{Proceedings,
@Comment Second Workshop on Higher Order Operational Techniques in Semantics
@Comment (HOOTS II), Stanford CA, December 1997}, Electronic Notes in
@Comment Theoretical Computer Science 10, 1998.}
@Comment }
@InProceedings{PittsAM:newaas,
author = {M.~J.~Gabbay and A.~M.~Pitts},
title = {A New Approach to Abstract Syntax Involving Binders},
booktitle = {14th Annual Symposium on Logic in Computer Science},
year = 1999,
publisher = {IEEE Computer Society Press, Washington},
pages = {214--224},
abstract = {The Fraenkel-Mostowski permutation model of set
theory with atoms (\emph{FM-sets}) can serve as the
semantic basis of meta-logics for specifying and
reasoning about formal systems involving name
binding, $\alpha$-conversion, capture avoiding
substitution, and so on. We show that in FM-set
theory one can express statements quantifying over
`fresh' names and we use this to give a novel
set-theoretic interpretation of name abstraction.
Inductively defined FM-sets involving this
name-abstraction set former (together with cartesian
product and disjoint union) can correctly encode
object-level syntax modulo $\alpha$-conversion. In
this way, the standard theory of algebraic data
types can be extended to encompass signatures
involving binding operators. In particular, there
is an associated notion of structural recursion for
defining syntax-manipulating functions (such as
capture avoiding substitution, set of free
variables, etc) and a notion of proof by structural
induction, both of which remain pleasingly close to
informal practice.}
}
@Comment inproceedings{Pittsam:Tritr,
@Comment Author = {A. M. Pitts},
@Comment Title = {Tripos Theory In Retrospect},
@Comment Booktitle = {Tutorial Workshop On Realizability Semantics,
@Comment {Floc'99}, Trento, Italy, 1999},
@Comment Editor = {L. Birkedal And G. Rosolini},
@Comment Volume = 23,
@Comment Number = 1,
@Comment Series = {Electronic Notes In Theoretical Computer Science},
@Comment Year = 1999,
@Comment Publisher = {Elsevier},
@Comment Url = {Http://Www.Elsevier.Nl/Cas/Tree/Store/Tcs/Free/Entcs/Store/Tcs23/1/Tcs23.1.010.Ps}
@Comment }
@Article{PittsAM:tritr,
author = {A. M. Pitts},
title = {Tripos Theory In Retrospect},
journal = {Mathematical Structures in Computer Science},
year = 2002,
volume = 12,
pages = {265--279}
}
@proceedings{PittsAM:hoots99,
editor = {A. Gordon and A. Pitts},
title = {Higher Order Operational Techniques in Semantics,
Third International Workshop, Paris, 1999},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
volume = 26,
year = 1999,
url =
{http://www.elsevier.nl/cas/tree/store/tcs/free/entcs/store/tcs26/cover.sub.sht}
}
@InProceedings{PittsAM:metpbn,
author = {A. M. Pitts and M. J. Gabbay},
title = {A Metalanguage for Programming with Bound Names
Modulo Renaming},
booktitle = {Mathematics of Program Construction. 5th
International Conference, MPC2000, Ponte de Lima,
Portugal, July 2000. Proceedings},
pages = {230--255},
year = 2000,
editor = {R. Backhouse and J. N. Oliveira},
volume = 1837,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag, Heidelberg},
doi = {10.1007/10722010_15}
}
@InProceedings{PittsAM:opeplp,
author = {G. M. Bierman and A. M. Pitts and C. V. Russo},
title = {Operational Properties of {Lily}, a Polymorphic
Linear Lambda Calculus with Recursion},
booktitle = {Fourth International Workshop on Higher Order
Operational Techniques in Semantics, Montr{\'e}al},
year = 2000,
volume = 41,
pages = {70--88},
series = {Electronic Notes in Theoretical Computer Science},
month = sep,
publisher = {Elsevier},
issn = {1571-0661}
}
@InCollection{PittsAM:opespe,
author = {A. M. Pitts},
title = {Operational Semantics and Program Equivalence},
booktitle = {Applied Semantics, Advanced Lectures},
pages = {378--412},
publisher = {Springer-Verlag},
year = 2002,
editor = {G. Barthe and P. Dybjer and J. Saraiva},
volume = 2395,
series = {Lecture Notes in Computer Science, Tutorial},
note = {International Summer School, {APPSEM} 2000, Caminha,
Portugal, September 9--15, 2000},
isbn = {3-540-44044-5}
}
@Article{PittsAM:newaas-jv,
author = {M. J. Gabbay and A. M. Pitts},
title = {A New Approach to Abstract Syntax with Variable
Binding},
journal = {Formal Aspects of Computing},
year = 2002,
volume = 13,
pages = {341--363},
doi = {10.1007/s001650200016},
url =
{http://www.springerlink.com/content/epn028x83rqw00qv/}
}
@InProceedings{PittsAM:firotn,
author = {A. M. Pitts},
title = {A First Order Theory of Names and Binding},
booktitle = {Mechanized Reasoning about Languages with Variable
Binding ({MERLIN} 20001), Procceedings of a Workshop
held in conjunction with the International Joint
Conference on Automated Reasoning, IJCAR 2001,
Siena, June 2001},
pages = {1--14},
year = 2001,
editor = {S. Ambler and R. Crole and A. Momigliano},
series = {Department of Computer Science Technical Report
2001/26},
organization = {University of Leicester}
}
@InProceedings{PittsAM:nomlfo,
author = {A. M. Pitts},
title = {Nominal Logic: A First Order Theory of Names and
Binding},
booktitle = {Theoretical Aspects of Computer Software, 4th
International Symposium, TACS 2001, Sendai, Japan,
October 29-31, 2001. Proceedings},
pages = {219--242},
year = 2001,
editor = {N. Kobayashi and B. C. Pierce},
volume = 2215,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag, Berlin},
isbn = {3-540-42736-8}
}
@Article{PittsAM:nomlfo-jv,
author = {A. M. Pitts},
title = {Nominal Logic, A First Order Theory of Names and
Binding},
journal = {Information and Computation},
year = 2003,
pages = {165--193},
volume = 186,
doi = {10.1016/S0890-5401(03)00138-X},
url = {http://dx.doi.org/10.1016/S0890-5401(03)00138-X}
}
@InProceedings{PittsAM:nomu,
author = {C. Urban and A. M. Pitts and M. J. Gabbay},
title = {Nominal Unification},
booktitle = {Computer Science Logic and 8th Kurt G{\"o}del
Colloquium (CSL'03 \& KGC), Vienna,
Austria. Proceedings},
pages = {513--527},
year = 2003,
editor = {M. Baaz},
volume = 2803,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag, Berlin}
}
@Article{PittsAM:nomu-jv,
author = {C. Urban and A. M. Pitts and M. J. Gabbay},
title = {Nominal Unification},
journal = {Theoretical Computer Science},
year = 2004,
volume = 323,
pages = {473--497},
doi = {10.1016/j.tcs.2004.06.016},
url = {http://dx.doi.org/10.1016/j.tcs.2004.06.016}
}
@InProceedings{PittsAM:frepbm,
author = {M. R. Shinwell and A. M. Pitts and M. J. Gabbay},
title = {Fresh{ML}: Programming with Binders Made Simple},
booktitle = {Eighth {ACM SIGPLAN} International Conference on
Functional Programming ({ICFP} 2003), Uppsala,
Sweden},
pages = {263--274},
year = 2003,
month = aug,
publisher = {ACM Press}
}
@TechReport{PittsAM:impccj,
author = {G.M. Bierman and M.J. Parkinson and A.M. Pitts},
title = {An Imperative Core Calculus for Java and Java with
Effects},
institution = {University of Cambridge Computer Laboratory},
year = 2003,
number = 563,
month = apr
}
@InCollection{PittsAM:typor,
author = {A. M. Pitts},
title = {Typed Operational Reasoning},
booktitle = {Advanced Topics in Types and Programming Languages},
pages = {245--289},
publisher = {The MIT Press},
year = 2005,
editor = {B. C. Pierce},
chapter = 7,
isbn = {0-262-16228-8}
}
@Comment Unpublished{PittsAM:densse,
@Comment author = {A. M. Pitts and T. Sheard},
@Comment title = {On the Denotational Semantics of Staged Execution of
@Comment Open Code},
@Comment note = {Submitted},
@Comment month = feb,
@Comment year = 2004
@Comment }
@Article{PittsAM:monsf,
author = {M. R. Shinwell and A. M. Pitts},
title = {On a Monadic Semantics for Freshness},
journal = {Theoretical Computer Science},
year = 2005,
volume = 342,
pages = {28--55},
doi = {10.1016/j.tcs.2005.06.003},
url = {http://dx.doi.org/10.1016/j.tcs.2005.06.003}
}
@TechReport{PittsAM:freocu,
author = {M. R. Shinwell and A. M. Pitts},
title = {{F}resh {O}bjective {C}aml User Manual},
institution = {University of Cambridge Computer Laboratory},
year = 2005,
number = {UCAM-CL-TR-621},
month = feb
}
@InProceedings{PittsAM:alpsri-ea,
author = {A. M. Pitts},
title = {Alpha-Structural Recursion and Induction (Extended
Abstract)},
booktitle = {Theorem Proving in Higher Order Logics, 18th
International Conference, TPHOLs 2005, Oxford UK,
August 2005, Proceedings},
pages = {17--34},
year = 2005,
editor = {J. Hurd and T. Melham},
volume = 3603,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@Article{PittsAM:alpsri,
author = {A. M. Pitts},
title = {Alpha-Structural Recursion and Induction},
journal = {Journal of the {ACM}},
year = 2006,
volume = 53,
pages = {459--506},
doi = {10.1145/1147954.1147961},
url = {http://doi.acm.org/10.1145/1147954.1147961}
}
@InProceedings{PittsAM:genun,
author = {A. M. Pitts and M. R. Shinwell},
title = {Generative Unbinding of Names},
booktitle = {34th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL 2007),
Nice, France},
pages = {85--95},
year = 2007,
month = jan,
publisher = {ACM Press}
}
@InCollection{PittsAM:nomel,
author = {R. A. Clouston and A. M. Pitts},
title = {Nominal Equational Logic},
booktitle = {Computation, Meaning and Logic, Articles dedicated
to Gordon Plotkin },
pages = {223--257},
publisher = {Elsevier},
year = 2007,
editor = {L. Cardelli and M. Fiore and G. Winskel},
volume = 1496,
series = {Electronic Notes in Theoretical Computer Science},
doi = {10.1016/j.entcs.2007.02.009}
}
@InProceedings{PittsAM:metsos,
author = {M. R. Lakin and A. M. Pitts},
title = {A Metalanguage for Structural Operational Semantics},
booktitle = {Eighth Symposium on Trends in Functional Programming
(TFP 2007), New York, USA},
pages = {{I-1}--{I-16}},
year = 2007,
month = apr,
note = {Draft proceedings}
}
@InCollection{PittsAM:metsos-jv,
author = {M. R. Lakin and A. M. Pitts},
title = {A Metalanguage for Structural Operational Semantics},
booktitle = {Trends in Functional Programming Volume 8},
editor = {M. Moraz{\'a}n},
year = 2008,
pages = {19--35},
publisher = {Intellect},
isbn = 9781841501963
}
@Article{PittsAM:genun-jv,
author = {A. M. Pitts and M. R. Shinwell},
title = {Generative Unbinding of Names},
journal = {Logical Methods in Computer Science},
year = 2008,
volume = 4,
number = {1:4},
pages = {1--33},
doi = {10.2168/LMCS-4(1:4)2008}
}
@InProceedings{PittsAM:residb,
author = {M. R. Lakin and A. M. Pitts},
title = {Resolving Inductive Definitions with Binders in
Higher-Order Typed Functional Programming},
booktitle = {18th European Symposium on Programming (ESOP~2009)},
editor = {G. Castagna},
pages = {47--61},
year = 2009,
volume = 5502,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@InProceedings{PittsAM:nomst-popl,
author = {A. M. Pitts},
title = {Nominal {System T}},
booktitle = {Proceedings of the 37th {ACM SIGACT-SIGPLAN}
Symposium on Principles of Programming Languages
(POPL 2010), Madrid, Spain},
pages = {159--170},
year = 2010,
month = jan,
publisher = {ACM Press},
doi = {10.1145/1706299.1706321}
}
@InProceedings{PittsAM:steibt,
author = {A. M. Pitts},
title = {Step-Indexed Biorthogonality: a Tutorial Example},
booktitle = {Modelling, Controlling and Reasoning About State},
year = 2010,
editor = {A. Ahmed and N. Benton and L. Birkedal and
M. Hofmann},
number = {10351},
series = {Dagstuhl Seminar Proceedings},
ISSN = {1862-4405},
publisher = {Schloss Dagstuhl---Leibniz-Zentrum fuer Informatik,
Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2010/2806},
annote = {Keywords: Biorthogonality, logical relations,
operational semantics, step-indexing}
}
@Article{PittsAM:encasw,
author = {M. R. Lakin and A. M. Pitts},
title = {Encoding Abstract Syntax without Fresh Names},
journal = {Journal of Automated Reasoning},
year = 2011,
volume = 49,
number = 2,
pages = {115--140},
url = {http://dx.doi.org/10.1007/s10817-011-9220-7}
}
@InCollection{PittsAM:howmho,
author = {A. M. Pitts},
editor = {D. Sangiorgi and J. Rutten},
title = {Howe's Method for Higher-Order Languages},
booktitle = {Advanced Topics in Bisimulation and Coinduction},
pages = {197--232},
publisher = {Cambridge University Press},
year = 2011,
volume = 52,
series = {Cambridge Tracts in Theoretical Computer Science},
chapter = 5,
month = nov,
isbn = {978-1-107-00497-9}
}
@Article{PittsAM:strrls,
author = {A. M. Pitts},
title = {Structural Recursion with Locally Scoped Names},
journal = {Journal of Functional Programming},
year = 2011,
volume = 21,
number = 3,
pages = {235--286},
url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=8279565}
}
@InProceedings{PittsAM:reltsl,
author = {S. L{\"o}sch and A. M. Pitts},
title = {{Relating Two Semantics of Locally Scoped Names}},
booktitle = {Computer Science Logic (CSL'11) - 25th International
Workshop/20th Annual Conference of the EACSL},
pages = {396--411},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
ISBN = {978-3-939897-32-3},
ISSN = {1868-8969},
year = {2011},
volume = {12},
editor = {Marc Bezem},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2011/3245},
URN = {urn:nbn:de:0030-drops-32454},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2011.396},
annote = {Keywords: local names, continuations, typed
lambda-calculus, observational equivalence}
}
@Article{PitssAM:lics2007,
author = {E. Gr{\"a}del and L. Ong and A. M. Pitts},
title = {Selected Papers of the Conference {`Logic in
Computer Science 2007'}},
journal = {Logical Methods in Computer Science},
year = 2010,
doi = {10.2168/LMCS-LICS:2007}
}
@Article{PitssAM:lics2009,
author = {R. Jagadeesan and N. Piterman and A. M. Pitts},
title = {Selected Papers of the Conference {`Logic in
Computer Science 2009'}},
journal = {Logical Methods in Computer Science},
year = 2011
}
@Proceedings{PittsAM:icalp2012-1,
title = {Automata, Languages, and Programming, 39th
International Colloquium, {ICALP} 2012, Warwick, UK,
Proceedings, Part {I}},
year = 2012,
editor = {A. Czumaj and K. Mehlhorn and A. M. Pitts and
R. Wattenhofer},
volume = 7391,
series = {Lecture Notes in Computer Science},
month = jul,
publisher = {Springer Berlin Heidelberg},
doi = {10.1007/978-3-642-31594-7}
}
@Proceedings{PittsAM:icalp2012-2,
title = {Automata, Languages, and Programming, 39th
International Colloquium, {ICALP} 2012, Warwick, UK
Proceedings, Part {II}},
year = 2012,
editor = {A. Czumaj and K. Mehlhorn and A. M. Pitts and
R. Wattenhofer},
volume = 7392,
series = {Lecture Notes in Computer Science},
month = jul,
publisher = {Springer Berlin Heidelberg},
doi = {10.1007/978-3-642-31585-5}
}
@InProceedings{PittsAM:fullans,
author = {S. L{\"o}sch and A. M. Pitts},
title = {Full Abstraction for Nominal Scott Domains},
booktitle = {Proceedings of the 40th {ACM SIGACT-SIGPLAN}
Symposium on Principles of Programming Languages
(POPL 2013), Rome, Italy},
pages = {3--14},
year = 2013,
editor = {R. Cousot},
month = {jan},
publisher = {ACM Press},
doi = {http://dx.doi.org/10.1145/2429069.2429073}
}
@Book{PittsAM:nomsns,
author = {A. M. Pitts},
title = {Nominal Sets: Names and Symmetry in Computer
Science},
publisher = {Cambridge University Press},
year = 2013,
volume = 57,
series = {Cambridge Tracts in Theoretical Computer Science},
isbn = {9781107017788}
}
@InProceedings{AhnKY:sysfi,
author = {K. Y. Ahn and T. Sheard and M. P. Fiore and
A. M. Pitts},
title = {System $F_i$},
booktitle = {Typed Lambda Calculi and Applications, 11th
International Conference, TLCA 2013, Eindhoven, The
Netherlands. Proceedings},
pages = {15--30},
year = {2013},
editor = {M. Hasegawa},
volume = 7941,
series = {Lecture Notes in Computer Science},
publisher = {Springer Berlin Heidelberg},
doi = {10.1007/978-3-642-38946-7_4}
}
@Article{PittsAM:coneid,
author = {M. R. Lakin and A. M. Pitts},
title = {Contextual Equivalence for Inductive Definitions
with Binders in Higher-Order Typed Functional
Programming},
journal = {Journal of Functional Programming},
year = {2013},
volume = 23,
number = 6,
pages = {658--700}
}
@Article{PittsAM:equpbc,
author = {A. M. Pitts},
title = {An Equivalent Presentation of the
{Bezem-Coquand-Huber} Category of Cubical Sets},
journal = {ArXiv e-prints},
year = {2013},
volume = {arXiv:1401.7807},
month = dec,
url = {http://arxiv.org/abs/1401.7807}
}
@Article{PittsAM:nomct,
author = {M. Bojanczyk and B. Klin and A. Kurz and A. M. Pitts},
title = {{Nominal Computation Theory (Dagstuhl Seminar 13422)}},
pages = {58--71},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2014},
volume = {3},
number = {10},
editor = {M. Bojanczyk and B. Klin and A. Kurz and A. M. Pitts},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2014/4428},
URN = {urn:nbn:de:0030-drops-44285},
doi = {http://dx.doi.org/10.4230/DagRep.3.10.58},
annote = {Keywords: nominal sets, Fraenkel-Mostowski sets}
}
@Article{PittsAM:densns,
author = {S. L{\"o}sch and A. M. Pitts},
title = {Denotational Semantics with Nominal Scott Domains},
journal = {Journal of the {ACM}},
year = 2014,
month = jul,
volume = 61,
number = 4,
doi = {http://dx.doi.org/10.1145/2629529},
pages = {27:1--27:46}
}
@InProceedings{PittsAM:deptta,
author = {A. M. Pitts and J. Matthiesen and J. Derikx},
title = {A Dependent Type Theory with Abstractable Names},
booktitle = {Proceedings of the 9th Workshop on Logical and
Semantic Frameworks, with Applications (LSFA 2014)},
year = 2015,
editor = {I. Mackie and M. Ayala-Rincon },
volume = 312,
series = {Electronic Notes in Theoretical Computer Science},
pages = {19--50},
doi = {http://dx.doi.org/10.1016/j.entcs.2015.04.003},
publisher = {Elsevier}
}
@InProceedings{PittsAM:nompcs,
author = {A. M. Pitts},
title = {{Nominal Presentation of Cubical Sets Models of Type
Theory}},
booktitle = {20th International Conference on Types for Proofs
and Programs (TYPES 2014)},
pages = {202--220},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
ISBN = {978-3-939897-88-0},
ISSN = {1868-8969},
year = {2015},
volume = {39},
editor = {H. Herbelin and P. Letouzey and M. Sozeau},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5498},
URN = {urn:nbn:de:0030-drops-54980},
doi = {http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.202},
annote = {Keywords: models of dependent type theory, homotopy
type theory, cubical sets, nominal sets, monoids}
}
@Proceedings{PittsAM:fossacs2015,
title = {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},
year = 2015,
editor = {A. M. Pitts},
volume = 9034,
series = {Lecture Notes in Computer Science},
month = apr,
publisher = {Springer-Verlag},
doi = {http://dx.doi.org/10.1007/978-3-662-46678-0}
}
@INPROCEEDINGS{PittsAM:namscs,
author = {Pitts, A.M.},
booktitle = {Logic in Computer Science ({LICS}), 2015 30th Annual
{ACM/IEEE} Symposium on},
title = {Names and Symmetry in Computer Science (Invited
Tutorial)},
year = {2015},
pages = {21-22},
doi = {10.1109/LICS.2015.12},
ISSN = {1043-6871},
month = {July},
publisher = {IEEE Computer Society Press}
}
@Article{PittsAM:nomt,
author = {A. M. Pitts},
title = {Nominal Techniques},
journal = {{ACM SIGLOG} News},
year = 2016,
volume = 3,
number = 1,
pages = {57--72},
month = jan
}
@InProceedings{PittsAM:aximct,
author = {I. Orton and A. M. Pitts},
title = {Axioms for Modelling Cubical Type Theory in a Topos},
booktitle = {25th EACSL Annual Conference on Computer Science
Logic ({CSL} 2016)},
editor = {J.-M. Talbot and L. Regnier},
year = 2016,
volume = 62,
editor = {L. Regnier nad J.-M. Talbot},
series = {Leibniz International Proceedings in Informatics
(LIPIcs)},
pages = {24:1--24:19},
address = {Dagstuhl, Germany},
doi = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.24},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f\"ur Informatik}
}