University of Birmingham > Talks@bham > Theoretical computer science seminar > Domain Theory in Constructive and Predicative Univalent Foundations

## Domain Theory in Constructive and Predicative Univalent FoundationsAdd to your list(s) Download to your calendar using vCal - Tom de Jong, School of Computer Science, University of Birmingham
- Thursday 14 January 2021, 13:45-15:00
- Zoom link at the bottom of the abstract.
If you have a question about this talk, please contact Martin Escardo. This is a Lab Lunch Talk. Notice that the Zoom link has changed. We meet at 13:45 to socialize and the talk starts at 14:00. We develop domain theory in constructive univalent foundations without Voevodsky’s resizing axioms. In work discussed in an earlier lablunch, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott’s D∞ model of the untyped λ-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF , the dcpos have carriers in the second universe 𝓤₁ and suprema of directed families with indexing type in the first universe 𝓤₀. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott’s D∞ again gives a large, locally small, algebraic dcpo with small directed suprema. I’m presenting a joint paper with Martin at CSL 2021 on 27 January. I would like to use the lab lunch to rehearse my talk. https://bham-ac-uk.zoom.us/j/81309745934 This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- Zoom link at the bottom of the abstract
- computer sience
Note that ex-directory lists are not shown. |
## Other listsApplied Topology Colloquium Speech Recognition by Synthesis Seminars IRLab Seminars: Robotics, Computer Vision & AI## Other talks[Colloquium:] Aperture Fever: The Extremely Large Telescope Module tensor categories and the Landau-Ginzburg/conformal field theory correspondence Theory: This is moved to next year, 2023 ! The science of the large scale heliosphere and the missions that made it possible Advancing biomedical photoacoustic imaging using structured light and optical microresonators TBC |