John Longley's research page

Completed papers

• 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), 469--505.

• (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), 333-352.

• 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), 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), 161-176.

• The sequentially realizable functionals, 93 pages (ps, pdf). In Annals of Pure and Applied Logic 117(1) (2002), 1-93.

• 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), 32-142.

• 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), 25-63.

• 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), 87-109. [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), 201-216.

• On the ubiquity of certain total type structures (full version), 113 pages (ps, pdf). In Mathematical Structures in Computer Science 17(5) (2007), 841--953.

• (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 (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 7-2006.

• (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 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, 117-134 (2009).

• 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). In Logical Methods in Computer Science 14(3:8), 1-51 (2018).

• Bar recursion is not computable via iteration, 43 pages (at arxiv.org/abs/1804.07277). Accepted for publication in Computability. 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 (at arxiv.org/abs/1806.00344). Unpublished paper (2018).

Slides from talks

• In what 2-category 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. (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.

Research grants

• (With Fourman and Plotkin) Notions of computability for general datatypes (1998-2000): proposal (ps, pdf) and final report (ps, pdf).

• (With Fourman and Fleuriot) A proof system for correct program development (2001-2004): proposal (ps, pdf) and final report (to appear soon).

• A programming language based on game semantics (started 2004): proposal (ps, pdf).