ABSTRACT. Brouwer’s induction theorems – the Fan Theorem and Bar Induction – which underpin his theory of the continuum, are often presented as postulates or axioms. For Brouwer they were foundational theorems. When proofs are given, modern presentations are generally proof-theoretic in character, whereas Brouwer presented his proofs, somewhat obscurely, as analyses of mathematical constructions. The induction theorems are constructively valid in suitable sheaf models. We argue that particular monoid models – based on the monoids of open endomorphisms of the formal Baire and Cantor spaces – provide an interpretation for intuitionistic quantification over spreads, non-classical mathematical entities introduced by Brouwer’s ‘second act of intuitionism’. We focus here on the Fan theorem and Cantor space, C – we anticipate that a similar analysis should apply to Bar Induction for Baire space. A topological model over T represents a choice sequence α as a continuous function α : T → C, a choice sequence corresponds to the species of its finite prefixes. An open map σ : C → T may be presented as an internal formal space that corresponds to a Brouwerian spread, and the spread is substantial iff the map is a surjection. Monoid models differ subtly from topological models. Topological models interpret quantification over sequences presented as species. We interpret the Joyal-Lawvere sheaf-theoretic interpretation of universal quantification in the monoid model of open endomorphisms of C as subsuming sequences introduced by substantial spreads. We outline a Brouwerian presentation of this model, and argue that this provides a Brouwerian proof – an argument that should have been acceptable to Brouwer – of the Fan Theorem.

ABSTRACT. Fifty years ago, Dana Scott and Christopher Strachey introduced denotational semantics as a way to specify program behavior, using domain theory and fixed-point principles to make sense of recursive definitions. These ideas have had enormous influence and have been developed extensively and applied to a wide variety of programming languages. We recall the foundational principles that underpin the denotational approach, and give a somewhat revisionist account of some of the landmark developments, with emphasis on concurrent programming languages. We introduce a denotational framework for relaxed memory concurrency, an area which is notoriously difficult to formalize program behavior, and we suggest some directions for further development.

ABSTRACT. This talk will highlight the most important results in domain theory from the perspective of program semantics and will explain why they play a crucial role in program extraction from proofs, a topic which, at first glance, seems to have little connection to domain theory. Surprisingly, Scott-domains suffice for the purpose of program extraction, even for the extraction of nondeterministic and concurrent programs.

ABSTRACT. A recurring question in computability theory has been whether one can identify a `canonical' notion of computable operation on data of some given kind. If the data are natural numbers (or equivalently finite strings over a finite alphabet), then the existence of such a canonical notion is of course what is claimed by the classical Church-Turing thesis. If the data are themselves of a higher-order nature, then the situation is much more complex, but work of Normann (2000) and Longley (2007) has shown that even widely divergent concepts of higher-order computability will often converge in the class of `hereditarily total' functionals they give rise to.

I will outline some recent extensions of these results that imply the existence of a similarly robust computability notion for many kinds of data arising in traditional mathematical practice, particularly complex analysis. To construct (for example) the space of analytic functions on a given complex domain, or some type of higher-order operators acting on this space, one typically needs recourse not just to function spaces, but also to subset and quotient types. These constitute a non-trivial extension from the point of view of computability theory: the computable functions on a subset S of T are not immediately determined by those on T, as there may well be computable functions on S with no computable extension to T. Nevertheless, our new results show that one still obtains a highly robust and `canonical' computability notion for a wide range of mathematical types arising in this way. For many types of interest, this accords with the notion arising in Type Two Effectivity, but our contribution is to show robustness with respect to variations in the choice of the underlying computability model.

Whilst we believe that our computability notion has good credentials, it is still not the only such notion on the market for the types we have in mind. Drawing on a theorem of Schroeder (2010), we shall advance the conjecture that it is in fact one of just two natural computability notions arising in the arena of (higher-order) classical analysis.

A draft paper covering much of the material to be discussed is available at:

http://homepages.inf.ed.ac.uk/jrl/Research/ubiquity-reloaded3.pdf

ABSTRACT. We explore representing the compact subsets of a given represented space by infinite sequences over Plotkin's \T. We show that computably compact computable metric spaces admit a representation of their compact subsets in such a way that compact sets are essentially underspecified points. We can even ensure that a name of an n-element compact set contains n-1 occurrences of \bot. We undergo this study effectively and show that such a T^\omega-representation is effectively obtained from structures of computably compact computable metric spaces.

Along the way, we introduce the notion of a computable dyadic subbase, and prove that every computably compact computable metric space admits a proper computable dyadic subbase. As an application, we prove some statements about the Weihrauch degree of closed choice for finite subsets of computably compact computable metric spaces.

ABSTRACT. Bicategories have been used for many years to model computational phenomena such as concurrency and binders. The collectivity, Bicat, of bicategories has the structure of a tricategory, which have occasionally appeared explicitly and more often implicitly in the programming semantics literature. But what is a weak n-category in general? Strict n-categories for arbitrary n have been used to model concurrency and in connection with rewriting. So it seems only a matter of time until weak n-categories for arbitrary n prove to be of value for programming semantics too. Here, we explore, enrich, and otherwise mildly generalise a prominent definition by Batanin, as refined by Leinster, together with the surrounding theory: they assumed knowledge of sophisticated mathematics, glossed over the inherent recursion, and did not consider the concerns of programming semantics.

ABSTRACT. We introduce the localic derivative of complex analytic functions in the sense of program logic, giving rise to a Stone duality result for these functions. This extends the related work on real-valued functions on real finite dimensional Euclidean spaces to functions of complex variables.