You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (Mar 19 2021 at 20:03):Friday, 22:00 UTC
Tim Hosgood (Mar 19 2021 at 20:03):Abstract:
Quantitative Type Theory combines linear types (where we keep track of how many times a variable is used) and dependent types (where we can keep track of properties of terms using types). This gives a logical system which is both expressive and precise with respect to the resource usage of programs and proofs, with a rich model theory. I will talk about data types in this setting, in the form of "resource-aware" polynomial functors and their initial algebras, and how "quantitative" induction can be derived from initiality. This is joint work with Georgi Nakov.