![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsApplied Mathematics Seminar Series IMA West Midlands Branch Condensed Matter Group MeetingsOther talksTBA TBA TBA Life : it’s out there, but what and why ? An introduction to τ-exceptional sequences Ultrafast Spectroscopy and Microscopy as probes of Energy Materials |