home search a-z help
University of Cambridge Andrew Pitts
On-line Publications
Department of Computer Science & Technology > Andrew Pitts > On-line Publications

On-line Publications of Andrew Pitts

in reverse chronological order.
PittsAM:locns [10.1145/3571210]

A. M. Pitts, Locally Nameless Sets. Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL, Article No. 17, pp 488–514, January 2023.

[abstract] [bib] [pdf (updated version, encorporating Corrigendum)][Agda code]


PittsAM:quoitq [10.46298/lmcs-18(2:15)2022]

M. P. Fiore, A. M. Pitts and S. C. Steenkamp, Quotients, Inductive Types and Quotient Inductive Types. Logical Methods in Computer Science, Volume 18, Issue 2, 2022 (special issue for FoSSaCS 2020).

[abstract] [bib] [pdf][Agda code]


PittsAM:coniau [10.4204/EPTCS.372.7]

A. M. Pitts and S. C. Steenkamp, Constructing Initial Algebras Using Inflationary Iteration. In K. Kishida (ed), Fourth International Conference on Applied Category Theory (ACT 2021), EPTCS 372(2022)88-102.

[abstract] [bib] [pdf][Agda code]


PittsAM:coniqi [10.1007/978-3-030-45231-5_14]

M. P. Fiore, A. M. Pitts and S. C. Steenkamp, Constructing Infinitary Quotient-Inductive Types. In J. Goubault-Larrecq and B. König (eds), Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), Dublin, Ireland, Lecture Notes in Computer Science Vol. 12077, pp 257-276 (Springer, 2020).

[abstract] [bib] [pdf] [Agda code]


PittsAM:typhet [10.1145/3379447]

A . M . Pitts, Typal Heterogeneous Equality Types, ACM Trans. Comput. Logic 21, 3, Article 25 (March 2020), 10 pages.

[abstract] [bib] [pdf] [Agda code]


PittsAM:moddtt [10.1017/S0960129519000197]

R. Clouston, B. Mannaa, R. E. Møgelberg, A. M. Pitts and B. Spitters, Modal Dependent Type Theory and Dependent Right Adjoints, Mathematical Structures in Computer Science 30(2)118-138, 2020.

[abstract] [bib] [pdf © 2019 CUP]


PittsAM:modttb-jv [10.23638/LMCS-15(1:2)2019]

I. Orton and A. M. Pitts, Models of Type Theory Based on Moore Paths Logical Methods in Computer Science, Volume 15(1)2019, pp 2:1-2:24 (special issue for FSCD 2017).

[abstract] [bib] [pdf]

(This is a revised and extended version of: I. Orton and A. M. Pitts, Models of Type Theory Based on Moore Paths, in D. Miller (ed), Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84, pp. 28:1-28:16, 2017.)


PittsAM:aximct-jv [10.23638/LMCS-14(4:23)2018]

I. Orton and A. M. Pitts, Axioms for Modelling Cubical Type Theory in a Topos, Logical Methods in Computer Science, Volume 14(4)2018, pp 23:1-23:33 (special issue for CSL 2016).

[abstract] [bib] [pdf] [Agda code]

(This is a revised and extended version of: I. Orton and A. M. Pitts, Axioms for Modelling Cubical Type Theory in a Topos, in J.-M. Talbot and L. Regnier (eds), Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 62, pp. 24:1-24:19, 2016.)


PittsAM:intumh [dx.doi.org/10.4230/LIPIcs.FSCD.2018.22]

D. R. Licata, I. Orton, A. M. Pitts and B. Spitters, Internal Universes in Models of Homotopy Type Theory. In H. Kirchner (ed), Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108, pp. 22:1-22:17, 2018.

[abstract] [bib] [pdf] [Agda code]


PittsAM:decua [dx.doi.org/10.4230/LIPIcs.TYPES.2017.6]

I. Orton and A. M. Pitts, Decomposing the Univalence Axiom. In A. Abel, F. Nordvall Forsberg and A. Kaposi (eds), 23rd International Conference on Types for Proofs and Programs (TYPES 2017), Post-Proceedings Volume, Leibniz International Proceedings in Informatics (LIPIcs), Vol. 104, pp. 6:1-6:19, 2018.

(This is the full version of I. Orton and A. M. Pitts, Axioms for Univalence.)

[abstract] [bib] [pdf] [Agda code]


PittsAM:axiu [ISBN 978-963-284-884-6]

I. Orton and A. M. Pitts, Axioms for Univalence. In A. Kaposi (ed), 23rd International Conference on Types for Proofs and Programs (TYPES 2017), Abstracts, Budapest, Hungary, 29 May - 1 June 2017, pages 85-86.

[bib] [pdf] [Agda code]


PittsAM:nomt [dx.doi.org/10.1145/2893582.2893594]

A. M. Pitts, Nominal Techniques, ACM SIGLOG News, January 2016, Vol. 3, No. 1, pp. 57-72.

[abstract] [bib] [pdf]


PittsAM:nompcs [dx.doi.org/10.4230/LIPIcs.TYPES.2014.202]

A. M. Pitts, Nominal Presentation of Cubical Sets Models of Type Theory. In H. Herbelin, P. Letouzey and M. Sozeau (eds), Proceedings of the 20th International Conference on Types for Proofs and Programs (TYPES 2014), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 39, pp. 202-220, 2015.

[abstract] [bib] [pdf]


PittsAM:deptta [doi:dx.doi.org/10.1016/j.entcs.2015.04.003]

A. M. Pitts, J. Matthiesen and J. Derikx, A Dependent Type Theory with Abstractable Names. In I. Mackie and M. Ayala-Rincon (eds), Proceedings of the 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014), Electronic Notes in Theoretical Computer Science 312(2015) 19-50.

[abstract] [bib] [pdf © 2015 The Authors. Published by Elsevier B.V.]


PittsAM:densns [doi:dx.doi.org/10.1145/2629529]

S. Lösch and A. M. Pitts, Denotational Semantics with Nominal Scott Domains, Journal of the ACM 61(4):27:1-27:46, 2014.

(This paper is a revised and expanded version of S. Lösch and A. M. Pitts, Full Abstraction for Nominal Scott Domains.)

[ACM DL article] [ACM DL bibliometrics] [abstract] [bib] [pdf © 2014 ACM. ]


PittsAM:nomct [doi:10.4230/DagRep.3.10.58]

M. Bojanczyk, B. Klin, A. Kurz and A. M. Pitts, Nominal Computation Theory (Dagstuhl Seminar 13422), Dagstuhl Reports, Vol. 3, Issue 10, pp. 58–71, 2014.

[abstract] [bib] [pdf]


PittsAM:equpbc [doi:doi.org/10.48550/arXiv.1401.7807]

A. M. Pitts, An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets, ArXiv e-prints, arXiv:1401.7807, December 2013.

[abstract] [bib] [pdf]


PittsAM:coneid [doi:10.1017/S0956796813000245]

M. R. Lakin and A. M. Pitts, Contextual Equivalence for Inductive Definitions with Binders in Higher-Order Typed Functional Programming, Journal of Functional Programming, 23(6): 658-700, 2013.

(This paper is a revised and expanded version of M. R. Lakin and A. M. Pitts, Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming.)

[abstract] [bib][pdf © 2013 CUP]


AhnKY:sysfi [doi:10.1007/978-3-642-38946-7_4]

K. Y. Ahn, T. Shead, M. P. Fiore and A. M. Pitts, System Fi. In M. Hasegawa (ed.), Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, Proceedings, Lecture Notes in Computer Science, Volume 7941, pages 15-30 (Springer, 2013).

[bib][pdf © 2013 Springer]


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][errata]


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).

[ACM DL article] [ACM DL bibliometrics] [abstract] [bib]


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).

[ACM DL article] [ACM DL bibliometrics] [abstract] [bib] [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].)


PittsAM:freocu

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]


PittsAM:monsf [doi:10.1016/j.tcs.2005.06.003]

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.]


PittsAM:typor

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]


PittsAM:frepbm [doi:10.1145/944705.944729]

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]


PittsAM:nomu [doi:10.1016/j.tcs.2004.06.016]

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 draft version]


PittsAM:impccj

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]


PittsAM:nomlfo [doi:10.1016/S0890-5401(03)00138-X]

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

Cited as part of the 2019 Alonzo Church Award.

[ abstract] [bib][draft version (pdf)] [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]


PittsAM:newaas-jv [doi:10.1007/s001650200016]

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.

Cited as part of the 2019 Alonzo Church Award. Recipient of a 2019 LICS Test-of-Time Award.

(This is an extended and revised version of PittsAM:newaas.)

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


PittsAM:opespe

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]


PittsAM:tritr [doi:10.1017/S096012950200364X]

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]


PittsAM:opeplp

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]


PittsAM:catl

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]


PittsAM:metpbn [doi:10.1007/10722010_15]

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]


PittsAM:parpoe [doi:10.1017/S0960129500003066]

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]


PittsAM:newaas [doi:10.1109/LICS.1999.782617]

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.

Recipient of a 2019 LICS Test-of-Time Award.

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


PittsAM:procbu

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)]


PittsAM:operfl

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]


PittsAM:higoot

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]


PittsAM:notlrb

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]


PittsAM:opebtp

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)]


PittsAM:semlc

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]


PittsAM:realvo

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]


PittsAM:relpod

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][pdf © 1996 Academic Press][errata]


PittsAM:fulatb

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]


PittsAM:compavm

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]


PittsAM:holls

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)]


PittsAM:coiprd

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)]


PittsAM:obsphown

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]


PittsAM:obspho

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]


PittsAM:intsoq

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][pdf]


PittsAM:evall

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]


PittsAM:newffcff

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)]


PittsAM:nontpt

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]


PittsAM:notcl

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

[pdf (5.7MB)]


PittsAM:notrpl [doi:10.1007/BF00370830]

A. M. Pitts and P. Taylor, A Note on Russell's Paradox in Locally Cartesian Closed Categories, Studia Logica 48(1989)377-387.

[bib] [pdf © 1989 Springer]


PittsAM:theccs

J. M. E. Hyland and A. M. Pitts, The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models, Contemporary Mathematics 92(1989)137-199.

[bib][pdf © 1989 AMS]


PittsAM:concfo [doi:10.1016/0168-0072(89)90007-9]

A. M. Pitts, Conceptual completeness for first-order Intuitionistic logic: an application of categorical logic, Annals of Pure and Applied Logic 41(1989)33-81

[bib][pdf © 1989 Elsevier]


PittsAM:appsec [doi:10.1112/plms/s3-57.3.433]

A. M. Pitts, Applications of Sup-Lattice Enriched Category Theory to Sheaf Theory, Proc. London Math. Soc. (1988) s3-57 (3): 433-480.

[bib][pdf © 1988 London Mathematical Society]


PittsAM:theccs

J. M. E. Hyland and A. M. Pitts, The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models, Contemporary Mathematics 92 (1989): 137-199.

[bib][pdf © 1987 American Mathematical Society]


PittsAM:polist

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]


PittsAM:reslfp [doi:10.1090/S0002-9947-1987-0869216-2 ]

M. Makkai and A. M. Pitts, Some Results on Locally Finitely Presentable Categories, Trans. Amer. Math. Soc. 299 (1987), 473-496.

[bib][pdf © 1987 American Mathematical Society ]


PittsAM:intccp

A. M. Pitts, Interpolation and Conceptual Completeness for Pretoposes via Category Theory. In D. W. Keuker, E. G. K. Lopez-Escobar and C. H. Smith (eds), Mathematical Logic and Theoretical Computer Science (CRC Press, 1987), pp 301--327.

[abstract] [bib][pdf © 1987 CRC Press]


PittsAM:procbt [http://www.numdam.org/item?id=CTGDC_1985__26_1_43_0]

A. M. Pitts, On Product and Change of Base for Toposes, Cahiers de Topologie et Géométrie Différentielle Catégoriques, 26 no. 1 (1985), p. 43-61.

[bib][pdf]


PittsAM:appomc [doi:10.1016/0022-4049(83)90047-6]

A. M. Pitts, An Application of Open Maps to Categorical Logic, Journal of Pure and Applied Algebra Volume 29(1983)313-326.

[bib][pdf © 1983 Elsevier]


PittsAM:amaich [doi:10.1016/0022-4049(83)90104-4]

A. M. Pitts, Amalgamation and Interpolation in the Category of Heyting Algebras, Journal of Pure and Applied Algebra Volume 29(1983)155-165.

[bib][pdf © 1983 Elsevier]


PittsAM:fuzsdn

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]


PittsAM:thet

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

[bib] [pdf]


PittsAM:trit

J.M.E. Hyland, P.T. Johnstone and A. M. Pitts, Triposes Theory, Math. Proc. Cambridge Philos. Soc. 88(1980)205--232.

[bib] [pdf © 1980 Cambridge Philos. Soc.]