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

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

Hi,

The second LFCS seminar today will start shortly:

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:

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

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.