Domain Theory in Constructive and Predicative Univalent Foundations

Add 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.