Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
%%% ==================================================================== %%% 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} }