Publications of Andrew Pitts
%%% ====================================================================
%%% BibTeX-file{
%%% author = "Andrew M. Pitts",
%%% date = "2004-02-10",
%%% 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={Cambridge Univ.},
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},
chapter = 2,
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}
}
@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}
}
@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
}
@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}
}
@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}
}
@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}
}
|
