View: session overviewtalk overviewside by side with other conferences

14:00 | Invited Talk: Scott Domains for Denotational Semantics and Program Extraction 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. |

14:40 | Robust computability notions for types arising in classical analysis 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 |

15:05 | T^\omega-representations of compact sets through dyadic subbases SPEAKER: Hideki Tsuiki 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. |

16:00 | Higher-dimensional categories: recursion on extensivity SPEAKER: Thomas Cottrell 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. |

16:25 | A logical view of complex analytic maps SPEAKER: Mehrdad Maleki 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. |

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).