John Longley's research page
Completed papers
 Realizability toposes and language semantics, 286 pages.
PhD thesis, University of Edinburgh, available as ECSLFCS95,332 (1995).
 (With Simon Finn and Michael Fourman) Partial functions in a
total setting, 20 pages.
In Journal of Automated Reasoning 18 (1997), 85104.
 (With Alex Simpson) A uniform approach to domain theory in
realizability models, 35 pages.
In Mathematical Structures in Computer Science 7 (1997),
469505.
 (With Gordon Plotkin) Logical full abstraction and PCF, 20 pages.
In J. Ginzburg, Z. Khasidashvili, C. Vogel, J.J. Levy, and E. Vallduvi
(editors),
Tbilisi Symposium on Logic, Language and Computation, SiLLI/CSLI (1997),
333352.
 Matching typed and untyped realizability.
In L. Birkedal, J. van Oosten, G. Rosolini, and D.S. Scott (editors),
Proceedings of Workshop on Realizability, Trento.
Electronic Notes in Theoretical Computer Science 23(1),
Elsevier (1999).
 Unifying typed and untyped realizability, 5 pages
(txt).
An unpublished electronic note which has enjoyed some circulation in
the research community.
 When is a functional program not a functional program?, 7 pages.
In Proceedings of the Fourth ACM SIGPLAN International Conference on
Functional Programming, Paris,
ACM Press (1999), 17.
 (With Furio Honsell, Donald Sannella and Andrzej Tarlecki)
Constructive data refinement in typed lambda calculus, 16 pages.
In Proceedings of FOSSACS 2000, Springer LNCS 1784 (2000),
161176.
 The sequentially realizable functionals, 93 pages
(ps, pdf).
In Annals of Pure and Applied Logic 117(1) (2002), 193.
 Notions of computability at higher types I, 110 pages
(ps, pdf).
In R. Cori, A. Razborov, S. Todorcevic, and C. Wood (editors),
Logic Colloquium 2000, Lecture Notes in Logic 19,
ASL (2005), 32142.
 Universal types and what they are good for, 39 pages
(ps, pdf).
In GQ Zhang, J. Lawson, Y.M. Liu and M.K. Luo (editors),
Domain theory, logic and computation: Proceedings of the 2nd
International Symposium on Domain Theory,
Semantic Structures in Computation 3, Kluwer (2003), 2563.
 On the ubiquity of certain total type structures, Extended abstract,
22 pages (ps,
pdf).
In M. Escardo and A. Jung (editors),
Proceedings of the Workshop on Domains VI, Birmingham,
Electronic Notes in Theoretical Computer Science 73,
Elsevier (2004), 87109. [See below for full version.]
 (With Randy Pollack) Reasoning about CBV functional programs
in Isabelle/HOL,
16 pages (ps,
pdf).
In K. Slind, A. Bunker, G. Gopalakrishnan (editors),
Theorem Proving in Higher Order Logics, 17th International Conference,
TPHOLs 2004, Utah, proceedings, Springer LNCS 3223 (2004),
201216.
 On the ubiquity of certain total type structures
(full version),
113 pages (ps,
pdf).
In Mathematical Structures in Computer Science 17(5) (2007),
841953.
 (With Nicholas Wolverson)
Game semantics for objectoriented languages: a progress report,
22 pages (ps, pdf).
Presented at GaLoP II, Seattle (2006).
 On the calculating power of Laplace's demon (Part I), 50 pages
(ps, pdf).
Draft paper: requires major reworking.
A preliminary (shorter) version (containing a major technical error)
appeared in A. Beckmann, U. Berger, B. Lowe and J.V. Tucker (editors),
Logical Approaches to Computational Barriers: Second Conference on
Computability in Europe, CiE 2006, Swansea (2006).
University of Wales Swansea Report Series, # CSR 72006.
 (With Nicholas Wolverson)
Eriskay: a programming language based on game semantics, 38 pages
(ps, pdf).
Presented at
GaLoP III,
Budapest, April 2008.
 Interpreting localized computational effects using operators of
higher type, extended abstract, 14 pages
(ps, pdf).
In A. Beckmann, C. Dimitracopoulos and B. Loewe (editors),
Logic and Theory of Algorithms, Fourth Conference on
Computability in Europe, CiE 2008, Athens, proceedings,
Springer LNCS 5028 (2008).
 Definition of the Lingay programming language (Version 0.2),
41 pages (pdf).
Published as Informatics Research Report EDIINFRR1283,
University of Edinburgh (2008).
 Some programming languages suggested by game models,
17 pages (pdf).
In Proc. 25th MFPS, Oxford,
Electronic Notes in Theoretical Computer Science 249,
117134 (2009).
 Computability structures, simulations and realizability,
40 pages (pdf).
In Mathematical Structures in Computer Science 24(2) (2014),
e240201 (49 pages).
 Bar recursion is not T+min definable,
18 pages (pdf).
Informatics Research Report EDIINFRR1420,
University of Edinburgh (2015).
This paper relies fairly heavily on material from the forthcoming book
by myself and Dag Normann; in the meantime,
the paper below provides much of the necessary background and context.
 The recursion hierarchy for PCF is strict,
48 pages (pdf,
report page).
Informatics Research Report EDIINFRR1421,
University of Edinburgh (2015).
Revised, corrected and expanded version of July 2016 (pdf),
submitted for publication.
 An intrinsic treatment of ubiquity phenomena in higherorder
computability models (Part I, draft version),
55 pages (pdf).
Work in progress (2017).
Slides from talks
 In what 2category do PCAs most naturally live?
(pdf).
Talk at PCARC workshop, 9 July 2010, Edinburgh.
 Analysing PCF and Kleene computability via sequential procedures
(pdf).
Theory Seminar, 6 July 2012, Birmingham.
Software
 Catchcont and friends.
(NJSML source file to accompany the
above paper on Eriskay.)

Stratagem: a cool ML program illustrating some surprising programming applications of recent ideas in game semantics.
 When is a functional program not a functional program?
(SML source file accompanying the above paper of the same title).
A walkthrough introduction to the sequentially realizable functionals.
Research grants
 (With Fourman and Plotkin) Notions of computability for general datatypes
(19982000):
proposal (ps,
pdf) and
final report (ps,
pdf).
 (With Fourman and Fleuriot) A proof system for correct program development
(20012004):
proposal (ps,
pdf) and
final report (to appear soon).
 A programming language based on game semantics (started 2004):
proposal (ps,
pdf).
John Longley
Last modified: Thu Jul 23 16:26:06 BST 2015