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

Domain Theory in Constructive and Predicative Univalent Foundations

Add to your list(s) Download to your calendar using vCal

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.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.