On-line Publications of Andrew Pitts

PittsAM:nomsns [ISBN:9781107017788]

A. M. Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge Tracts in Theoretical Computer Science, vol. 57 (CUP, 2013), 276+xiv pages.

[bib]

PittsAM:fullans [doi:10.1145/2429069.2429073]

S. Lösch and A. M. Pitts, Full Abstraction for Nominal Scott Domains. In Proceedings of the 40th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2013), Rome, Italy, pages 3-14 (ACM Press, 2013).

[abstract] [bib] [pdf © 2013 ACM. This is the authors' version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. ]

PittsAM:encasw [doi:10.1007/s10817-011-9220-7]

M. R. Lakin and A. M. Pitts, Encoding Abstract Syntax without Fresh Names, Journal of Automated Reasoning 49(2) (2012) 115-140, special issue on Binding, Substitution and Naming.

[abstract] [bib] [pdf © 2012 Springer Netherlands. Draft version. ]

PittsAM:reltsl [doi:10.4230/LIPIcs.CSL.2011.396]

S. Lösch and A. M. Pitts, Relating Two Semantics of Locally Scoped Names. In M. Bezem (ed.), Proceedings of the 20th Conference on Computer Science Logic (CSL 2011), September 2011, Bergen, Norway, pages 396-411. Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany.

[abstract] [bib] [pdf]

PittsAM:strrls [doi:10.1017/S0956796811000116]

A. M. Pitts, Structural Recursion with Locally Scoped Names, Journal of Functional Programming, 21 (3): 235-286, 2011.

(This paper is a revised and expanded version of A. M. Pitts, Nominal System T.)

[abstract] [bib] [pdf © 2011 CUP. ]

PittsAM:howmho

A. M. Pitts, Howe's Method for Higher-Order Languages. In D. Sangiorgi and J. Rutten (eds), Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts in Theoretical Computer Science No. 52, chapter 5, pages 197--232 (Cambridge University Press, 2011).

[bib] [pdf © 2011 CUP. Draft version. ] [errata]

PittsAM:steibt

A. M. Pitts, Step-Indexed Biorthogonality: a Tutorial Example. In A. Ahmed, N. Benton, L. Birkedal and M. Hofmann (eds), Modelling, Controlling and Reasoning About State, Dagstuhl Seminar Proceedings 10351 (Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2010).

[abstract] [bib] [pdf]

PittsAM:nomst [doi:10.1145/1706299.1706321]

A. M. Pitts, Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), Madrid, Spain, pages 159-170 (ACM Press, 2010).

[abstract] [bib] [pdf © 2010 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. ] [Fresh Objective Caml code]

PittsAM:residb [doi:10.1007/978-3-642-00590-9_4]

M. R. Lakin and A. M. Pitts, Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming. In 18th European Symposium on Programming (ESOP 2009), York, UK, Lecture Notes in Computer Science, Volume 5502, pages 47-61 (Springer-Verlag, 2009).

[abstract] [bib] [pdf © 2009 Springer-Verlag]

PittsAM:genun-jv [doi:10.2168/LMCS-4(1:4)2008]

A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names, Logical Methods in Computer Science, Vol. 4 (1:4) 2008, pp. 1-33.

[abstract] [bib] [pdf]

(This is a revised and extended version of: A. M. Pitts and M. R. Shinwell, Generative Unbinding of Names. In 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, pages 85-95 (ACM Press, 2007). [doi:10.1145/1190216.1190232])

PittsAM:metsos-jv

M. R. Lakin and A. M. Pitts, A Metalanguage for Structural Operational Semantics. In M. T. Morazan (ed.), Trends in Functional Programming Volume 8, selected papers from the Eighth Symposium on Trends in Functional Programming (TFP 2007), New York, USA, April 2007, pages 19-35 (Intellect, 2008).

[abstract] [bib] [pdf]

PittsAM:nomel [doi:10.1016/j.entcs.2007.02.009]

R. A. Clouston and A. M. Pitts, Nominal Equational Logic. In L. Cardelli, M. Fiore and G. Winskel (eds) Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin , Electronic Notes in Theoretical Computer Science, Volume 172, pages 223-257 (Elsevier, 2007).

[abstract] [bib] [pdf © 2007 Elsevier B.V.]

PittsAM:alpsri [doi:10.1145/1147954.1147961]

A. M. Pitts, Alpha-Structural Recursion and Induction, Journal of the ACM 53(2006)459-506.

[abstract] [bib] [pdf © 2006 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.]

(This is a revised and extended version of: A. M. Pitts, Alpha-Structural Recursion and Induction (Extended Abstract), in J Hurd and T. Melham (Eds), 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, Oxford, UK, August 2005, Lecture Notes in Computer Science, Volume 3603 (Springer-Verlag, 2005), pages 17-34. [pdf © 2005 Springer-Verlag].)

M. R. Shinwell and A. M. Pitts, Fresh Objective Caml User Manual, University of Cambridge Computer Laboratory Technical Report UCAM-CL-TR-621, February 2005.

[abstract] [bib] [pdf]

M. R. Shinwell and A. M. Pitts, On a Monadic Semantics for Freshness, Theoretical Computer Science 342(2005) 28-55.

(A preliminary version appeared in Second workshop of FP5 IST thematic network IST-2001-38957 APPSEM II, Tallinn, Estonia, April 2004.)

[abstract] [bib] [pdf© 2006 Elsevier B. V.]

A. M. Pitts, Typed Operational Reasoning. In B. Pierce (ed), Advanced Topics in Types and Programming Languages, chapter 7, pages 245-289 (MIT Press, 2005).

(This is a revised and expanded version of: A. M. Pitts, Existential Types: Logical Relations and Operational Equivalence. In K. Larsen, S. Skyum and G. Winskel (Eds), Proc. ICALP'98, Lecure Notes in Computer Science, Volume 1443 (Springer-Verlag, 1998), pages 309-326.)

[Abstract] [bib] [pdf] [errata]

M. R. Shinwell, A. M. Pitts and M.J.Gabbay, FreshML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pages 263-274 (ACM Press, 2003).

Note the erratum to this paper.

[abstract] [bib] [pdf © 2003 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.] [erratum]

C.Urban, A. M.Pitts and M.J.Gabbay, Nominal Unification, Theoretical Computer Science 323(2004) 473-497.

(A preliminary version apeared in M.Baaz (Ed.), Computer Science Logic and 8th Kurt Godel Colloquium (CSL'03 & KGC), Vienna, Austria. Proccedings. Lecture Notes in Computer Science, Volume 2803, pages 513-527 (Springer-Verlag, 2003).)

See here for formal verification of the results in this paper, carried out by Urban using Isabelle.

[abstract] [bib][pdf© 2004 Elsevier B. V.]

G.M. Bierman, M.J. Parkinson and A. M. Pitts An Imperative Core Calculus for Java and Java with Effects. Technical Report number 563, University of Cambridge Computer Laboratory, April 2003.

[ abstract] [bib][pdf]

A. M. Pitts, Nominal Logic, A First Order Theory of Names and Binding, Information and Computation 186(2003) 165-193. Special issue on TACS2001.

[ abstract] [bib][pdf © 2003 Elsevier B. V.] [errata]

A preliminary version of this paper appeared in: N. Kobayashi and B. C. Pierce (Eds), Fourth International Symposium on Theoretical Aspects of Computer Software (TACS 20001), Sendai, Japan, October 2001. Proceedings. Lecture Notes in Computer Science, Volume 2215, pages 219-242 (Springer-Verlag, 2001). (Note! The version of the paper that appeared in the printed volume 2215 is deprecated because of font substitution problems; see here for more details.)

[pdf © 2001 Springer-Verlag]

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing 13(2002)341-363, special issue in honour of Rod Burstall. (This is an extended and revised version of PittsAM:newaas.)

[ abstract] [bib][pdf © 2001 BCS]

A. M. Pitts, Operational Semantics and Program Equivalence. In: G. Barthe, P. Dybjer and J. Saraiva (Eds), Applied Semantics. Lecture Notes in Computer Science, Tutorial, Volume 2395 (Springer-Verlag, 2002), pages 378-412. (Revised version of lectures at the International Summer School On Applied Semantics, APPSEM 2000, Caminha, Minho, Portugal, 9-15 September 2000.)

[pdf © 2002 Springer-Verlag] [course web page]

A. M. Pitts, Tripos Theory in Retrospect, Mathematical Structures in Computer Science 12(2002) 265-279. (A preliminary version appeared in Proceedings of the Tutorial Workshop on Realizability Semantics, FLoC'99, Trento, Italy, July 1999. Electronic Notes in Theoretical Computer Science 23 No.1 (1999).)

[abstract][bib][pdf © 2001 CUP]

G.M.Bierman, A. M. Pitts and C.V.Russo, Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion. In Proceedings, Fourth International Workshop on Higher Order Operational Techniques in Semantics (HOOTS 2000), Montreal, Canada, September 2000, Electronic Notes in Theoretical Computer Science 41(2000), p70-88.

[ abstract] [bib][pdf © 2000 Springer-Verlag]

A. M. Pitts, Categorical Logic. Chapter 2 of S. Abramsky and D. M. Gabbay and T. S. E. Maibaum (Eds) Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures, Oxford University Press, 2000. (A preliminary version appeared as Cambridge University Computer Laboratory Tech. Rept. No. 367, May 1995.)

[abstract][bib]

A. M. Pitts and M. J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming. In R. Backhouse and J. N. Oliveira (Eds), Mathematics of Programme Construction, 5th International Conference, MPC2000, Ponte de Lima, Portugal, July 2000. Proceedings. Lecture Notes in Computer Science, Volume 1837 (Springer-Verlag, 2000), pages 230-255.

[abstract][ bib][pdf © 2000 Springer-Verlag]

A. M. Pitts, Parametric Polymorphism and Operational Equivalence, Mathematical Structures in Computer Science 10(2000) 321-359. (A preliminary version appeared in Proceedings, Second Workshop on Higher Order Operational Techniques in Semantics (HOOTS II), Stanford CA, December 1997, Electronic Notes in Theoretical Computer Science 10(1998).)

[abstract][bib][pdf © 2000 CUP]

M.J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax Involving Binders. In Proceedings 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 1999, (IEEE Computer Society Press, 1999) pp 214-224.

[abstract][bib][pdf © 1999 IEEE]

A. M. Pitts and J.R.X. Ross, Process Calculus Based Upon Evaluation to Committed Form, Theoretical Computer Science 195(1998) 155-182. (A preliminary version of this paper appeared in CONCUR'96, Lecture Notes in Computer Science Vol. 1119 (Springer-Verlag, Berlin, 1996), pp 18-33.)

[abstract][bib][draft version (pdf)]

A. M. Pitts and I.D.B. Stark, Operational Reasoning for Functions with Local State. In A.D. Gordon and A. M. Pitts (Eds), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute (Cambridge University Press, 1998), pp 227-273.

[abstract][bib][pdf © 1998 CUP]

A.D. Gordon and A. M. Pitts (Eds), Higher Order Operational Techniques in Semantics, Publications of the Newton Institute (Cambridge University Press, 1998). ISBN 0-521-63168-8.

[bib][more details]

A. M. Pitts, A Note on Logical Relations Between Semantics and Syntax, Logic Journal of the Interest Group in Pure and Applied Logics 5(1997) 589--601.

[abstract][bib][pdf© 1997 OUP]

A. M.Pitts, Operationally-Based Theories of Program Equivalence,. In A. M. Pitts and P. Dybjer (Eds), Semantics and Logics of Computation, (Cambridge University Press, 1997), pp 241-298.

[abstract][bib][pdf © 1997 CUP] [errata (pdf)]

A. M. Pitts and P. Dybjer (Eds), Semantics and Logics of Computation, Publications of the Newton Institute (Cambridge University Press, 1997). ISBN 0-521-58057-9.

[bib][more details]

A. M. Pitts, Reasoning About Local Variables with Operationally-Based Logical Relations. In P.W. O'Hearn and R.D. Tennent (Eds), Algol-Like Languages, Volume 2 (Birkhauser, 1997), Chapter 17, pp 173-193. (Reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, Brunswick, NJ, July 1996, (IEEE Computer Society Press, 1996), pp 152-163.)

[Abstract][bib][pdf © 1996 IEEE]

A. M. Pitts, Relational Properties of Domains, Information and Computation 127(1996) 66--90. (A preliminary version of this work appeared as Cambridge Univ. Computer Laboratory Tech. Rept. No. 321, December 1993.)

[abstract][bib][draft version (pdf)]

E. Ritter and A. M. Pitts, A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML,. In 2nd Int. Conf. on Typed Lambda Calculus and Applications, Edinburgh, 1995, Lecture Notes in Computer Science Vol. 902 (Springer-Verlag, Berlin, 1995), pp 397-413.

[abstract][bib][pdf © 1995 Springer-Verlag]

A. M. Pitts, Computational Adequacy via `Mixed' Inductive Definitions,. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., New Orleans, LA, USA, April 1993, Lecture Notes in Computer Science, Vol. 802 (Springer-Verlag, Berlin, 1994), pp 72-82.

[abstract][bib][pdf © 1994 Springer-Verlag]

M. J. Gordon and A. M. Pitts, The HOL Logic and System. In J. Bowen (ed.), Towards Verified Systems (Elsevier Science B. V., 1994), chapter 3, pp 49-70.

[bib] [draft version (pdf)]

A. M.Pitts, A Co-induction Principle for Recursively Defined Domains, Theoretical Computer Science 124(1994) 195-219. (A preliminary version of this work appeared as Cambridge Univ. Computer Laboratory Tech. Rept. No. 252, April 1992.)

[ abstract][bib][draft version (pdf)]

A. M. Pitts and I.D.B. Stark, Observable Properties of Higher Order Functions That Dynamically Create Local Names, or: What's new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdansk, 1993, Lecture Notes in Computer Science Vol. 711 (Springer-Verlag, Berlin, 1993), pp 122-141.

[abstract][bib][pdf © 1993 Springer-Verlag]

A. M. Pitts and I.D.B. Stark, On the Observable Properties of Higher Order Functions That Dynamically Create Local Names (Preliminary Report),. In ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, 1993, Yale Univ. Dept. Computer Science Technical Report YALEU/DCS/RR-968, 1993, pp 31-45.

[abstract][bib][pdf]

A. M. Pitts, On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional Logic, Jour. Symbolic Logic 57(1992) 33-52.

[abstract][bib][draft version (pdf)]

A. M. Pitts, Evaluation Logic. In G. Birtwistle (Ed.), IVth Higher Order Workshop, Banff, 1990, Workshops in Computing (Springer-Verlag, Berlin, 1991), pp 162-189.

[abstract][bib][pdf © 1991 Springer-Verlag]

R.L. Crole and A. M. Pitts, New Foundations for Fixpoint Computations: FIX-hyperdoctrines and the FIX-logic, Information and Computation 98(1992) 171-210. (A preliminary version of these results was presented in: R.L. Crole and A. M. Pitts. New foundations for fixpoint computations. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 489-497, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.)

[bib] [draft version (pdf)]

A. M. Pitts, Non-trivial Power Types Can't Be Subtypes of Polymorphic Types. In Proceedings Fourth Annual IEEE Symposium on Logic in Computer Science, Asilomar, CA, July 1989, pp 6-13 (IEEE Computer Society Press, 1989).

[abstract][bib][pdf © 1989 IEEE]

A. M. Pitts, Notes on Categorical Logic. Unpublished lecture notes (1989).

[pdf (5.7MB)]

A. M. Pitts, Polymorphism is Set Theoretic, Constructively. In Category Theory and Computer Science, Proceedings, Edinburgh 1987, Lecture Notes in Computer Science Vol. 283 (Springer-Verlag, Berlin, 1987), pp 12-39.

[abstract][bib][pdf © 1987 Springer-Verlag]

A. M. Pitts, Fuzzy Sets Do Not Form a Topos, Short Communication, Fuzzy Sets and Systems 8(1982) 101-104.

[abstract] [bib] [pdf © 1982 North-Holland]

A. M. Pitts, The Theory of Triposes. PhD thesis, University of Cambridge, 1981.

[bib] [pdf]