John Longley's research page
- Realizability toposes and language semantics, 286 pages.
PhD thesis, University of Edinburgh, available as ECS-LFCS-95,332 (1995).
- (With Simon Finn and Michael Fourman) Partial functions in a
total setting, 20 pages.
In Journal of Automated Reasoning 18 (1997), 85-104.
- (With Alex Simpson) A uniform approach to domain theory in
realizability models, 35 pages.
In Mathematical Structures in Computer Science 7 (1997),
- (With Gordon Plotkin) Logical full abstraction and PCF, 20 pages.
In J. Ginzburg, Z. Khasidashvili, C. Vogel, J.-J. Levy, and E. Vallduvi
Tbilisi Symposium on Logic, Language and Computation, SiLLI/CSLI (1997),
- 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),
- Unifying typed and untyped realizability, 5 pages
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), 1-7.
- (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),
- The sequentially realizable functionals, 93 pages
In Annals of Pure and Applied Logic 117(1) (2002), 1-93.
- Notions of computability at higher types I, 110 pages
In R. Cori, A. Razborov, S. Todorcevic, and C. Wood (editors),
Logic Colloquium 2000, Lecture Notes in Logic 19,
ASL (2005), 32-142.
- Universal types and what they are good for, 39 pages
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), 25-63.
- On the ubiquity of certain total type structures, Extended abstract,
22 pages (ps,
In M. Escardo and A. Jung (editors),
Proceedings of the Workshop on Domains VI, Birmingham,
Electronic Notes in Theoretical Computer Science 73,
Elsevier (2004), 87-109. [See below for full version.]
- (With Randy Pollack) Reasoning about CBV functional programs
16 pages (ps,
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),
- On the ubiquity of certain total type structures
113 pages (ps,
In Mathematical Structures in Computer Science 17(5) (2007),
- (With Nicholas Wolverson)
Game semantics for object-oriented 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
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 7-2006.
- (With Nicholas Wolverson)
Eriskay: a programming language based on game semantics, 38 pages
Budapest, April 2008.
- Interpreting localized computational effects using operators of
higher type, extended abstract, 14 pages
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 EDI-INF-RR-1283,
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,
- Computability structures, simulations and realizability,
40 pages (pdf).
In Mathematical Structures in Computer Science 24(2) (2014),
e240201 (49 pages).
- The recursion hierarchy for PCF is strict,
60 pages (at arxiv.org/abs/1607.04611).
To appear in Logical Methods in Computer Science (special issue on
Domain Theory and its Applications). This version June 2018.
An earlier version appeared as Informatics Research Report
EDI-INF-RR-1421, University of Edinburgh (2015).
- Bar recursion is not computable via iteration,
43 pages (at arxiv.org/abs/1804.07277).
Submitted for publication April 2018.
Supersedes Bar recursion is not T+min definable,
18 pages (pdf),
Informatics Research Report EDI-INF-RR-1420,
University of Edinburgh (2015).
- An intrinsic treatment of ubiquity phenomena in higher-order
computability models (Part I, draft version),
55 pages (pdf).
Work in progress (2017).
- The encodability hierarchy for PCF types, 19 pages
Unpublished paper (2018).
Slides from talks
- In what 2-category do PCAs most naturally live?
Talk at PCARC workshop, 9 July 2010, Edinburgh.
- Analysing PCF and Kleene computability via sequential procedures
Theory Seminar, 6 July 2012, Birmingham.
- Catchcont and friends.
(NJ-SML 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.
- (With Fourman and Plotkin) Notions of computability for general datatypes
final report (ps,
- (With Fourman and Fleuriot) A proof system for correct program development
final report (to appear soon).
- A programming language based on game semantics (started 2004):
Last modified: Thu Jul 23 16:26:06 BST 2015