Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have **two** LFCS seminars next week on Tuesday:

1) Tuesday, 27 May, 2.10pm (note unusual time)

   Swagato Sanyal, University of Sheffield

   The seminar will take place in-person only.

   Venue: IF MF2

   If you want to meet with the speaker, contact Heng Guo <hguo@inf.ed.ac.uk> .

2) Tuesday, 27 May, 4.10pm

   Ayberk Tosun, University of Birmingham

   This seminar is hybrid.

  Venue: IF G.03

  To attend remotely:

  URL: https://ed-ac-uk.zoom.us/j/81130676089

  Password: i11ggQh6

  Contact me if you want to meet with Tosun, who is visiting

  Tuesday 27 May - Thursday 29 May.

We're synchronising the seminar time with the teaching timetable, and

plan to start the talk at the advertised time, so please arrive a minute or two

earlier.

In detail:

----------------------------------------------------------------------

Swagato Sanyal, University of Sheffield

https://www.sheffield.ac.uk/cs/people/academic/swagato-sanyal

  Tue, 27 May, 2.10pm

  Venue: IF MF-2

  Note unusual time and room.

Title: On the composition question for randomized query complexity.

Abstract

A query algorithm (also known as a decision tree) that computes a

Boolean function f on n variables, queries various bits of an input to f,

possibly in an adaptive fashion and using randomness. It eventually

produces a bit as an output, which is supposed to equal the value of f on

that input with high probability. The complexity measure of such an

algorithm is the number of queries that it makes in the worst case. This

talk considers the query complexity of a class of Boolean function

called 'composed functions'. Composition of two Boolean functions f

and g is, informally speaking, the Boolean function (say h) obtained by

successive applications of g and f. The composition question,

instantiated for query complexity, asks whether there exists a query

algorithm that computes h that is significantly more efficient than

what the definition of h suggests: first compute g and then compute f.

The question has been the centre of a lot of research, and stands open to

this day. In this work we present some results in relation to this

question.

----------------------------------------------------------------------

Ayberk Tosun, University of Birmingham

https://ayberkt.xyz/

  Tue, 27 May, 4.10pm

  Venue: IF G.03

  Remote participation:

  URL: https://ed-ac-uk.zoom.us/j/81130676089

  Password: i11ggQh6

Title: Constructive and Predicative Locale Theory in Univalent Foundations

Abstract

Univalent foundations (also known as homotopy type theory or HoTT/UF)

is a variant of Martin-Löf Type Theory that introduces several

novelties, which turn out to be particularly well-suited for the

development of constructive and predicative mathematics. In this

talk, I will present my doctoral work with Martín Escardó on the

constructive and predicative development of point-free topology

within the foundational setting of HoTT/UF, with a particular focus on

the theory of spectral and Stone locales. Specifically, I will explain

how the theory of spectral and Stone locales can be developed in a fully

constructive and predicative manner in HoTT/UF, and I will present two

applications of this framework: (1) a predicative version of the Stone

duality for spectral locales, and (2) a predicative construction of

the patch locale of a spectral locale, which universally transforms it

into a Stone locale. I will then discuss how this framework can be used to

investigate the constructive topology of domains, and will present a

new, topological characterization of Tom de Jong’s notion of sharp

element, formulated in terms of the patch locale of the Scott locale of a

Scott domain. Time permitting, I will also discuss some ongoing work on

the constructive treatment of the Lawson topology of a Scott domain.

All the results to be presented in this talk have been fully formalized

in the Agda proof assistant, as part of Escardó’s TypeTopology

library.

----------------------------------------------------------------------

Upcoming seminars:

------------------

05 Jun (Thur): Rasmus Møgelberg, IT University of Copenhagen

17 Jun (11.10am, TBC): Andreas Abel, Gothenburg University / Chalmers

05 Aug: Michael Sperber, Active Group GmbH

If you would like to propose a speaker, or speak yourself, please contact me.

The seminar webpages:

http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,

Ohad.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.