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.
Jon Sterling (May 04 2021 at 11:17):Recent activities:
Current activities:
Mike Shulman (May 04 2021 at 17:35):Thanks for the links to your recent talk; I was sorry to miss it. I am amused by the inverse video trick halfway through.
I assume it's not a coincidence that you used the same example of list queues and batched queues that appears in ACMZ Internalizing Representation Independence with Univalence. What is your feeling about the relative advantages and disadvantages of proving results of this sort using parametricity relations on inequivalent types (synthetically or not), versus quotienting the types to make them equivalent and applying univalence? As a mathematician, the latter feels much more natural to me....
Jon Sterling (May 04 2021 at 22:36):Mike Shulman said:
Thanks for the links to your recent talk; I was sorry to miss it. I am amused by the inverse video trick halfway through.
I assume it's not a coincidence that you used the same example of list queues and batched queues that appears in ACMZ Internalizing Representation Independence with Univalence. What is your feeling about the relative advantages and disadvantages of proving results of this sort using parametricity relations on inequivalent types (synthetically or not), versus quotienting the types to make them equivalent and applying univalence? As a mathematician, the latter feels much more natural to me....
Personally I find the approach via univalence to be more compelling --- when it works... It was surprising to me that so many cases of representation independence can be recovered if you quotient the representation types, though it now seems obvious in hindsight. Parametricity is, to me, fundamentally about proving things that hold in some restricted sense (e.g. on closed terms, etc.) _only_ by virtue of definability --- for instance, classifying all the closed implementations of a given polymorphic type, etc. The queue example is, from this standpoint, not as convincing but I continue to use it because it is very familiar and comfortable to PL people.
Mike Shulman (May 05 2021 at 03:26):I see, that makes sense!
Jon Sterling (May 25 2021 at 14:43):Just wanted to mention that I will be giving a talk in a little less than an hour in the Padova Logic Seminar about my joint work with Carlo Anguli, Normalization for Cubical Type Theory.
Time: 5:30PM Italian
https://unipd.zoom.us/j/83629916946?pwd=N3NyRTdIQjNBd1BsV2hXcTFPUU5DQT09
Meeting ID: 836 2991 6946
Passcode: 717658
ABSTRACT:
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. The main difficulty in comparison to conventional type theory is located in a new feature of cubical type theories, the absence of a stable notion of neutral term: for instance, the path application (p @ i) ceases to be neutral within its “locus of instability” ∂(i) and must compute to an endpoint. We introduce a new, geometrically-inspired generalization of the notion of neutral term, stabilizing neutrals by gluing them together with partial computability data along their loci of instability — when the locus of instability is nowhere, a stabilized neutral is a conventional neutral, and when the locus of instability is everywhere, a stabilized neutral is just computability data. Our normalization result is based on a reduction-free Artin gluing argument, and yields an injective function from equivalence classes of terms in context to a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality, as well as injectivity of type constructors in contexts formed by assuming variables x : A and dimensions i : 𝕀.
Cody Roux (May 25 2021 at 21:39):Any change we can get the slides? Or was this a write down as you speak type deal?
Jon Sterling (May 27 2021 at 00:16):Cody Roux said:
Any change we can get the slides? Or was this a write down as you speak type deal?
It was a chalk talk, yeah.
Jon Sterling (Jun 02 2021 at 11:20):Carlo and I have uploaded the video for our LICS '21 talk on cubical normalization to YouTube (available in 4K lol!)
Normalization for Cubical Type Theory (LICS 2021)
https://www.youtube.com/watch?v=g7EuLw9E8A8
David Michael Roberts (Jun 07 2021 at 11:25):The citation to "Sterling"/[Ste21] (made me chuckle) on the last slide on the univalent version: is that available/soon available/just over the next rise?
Jon Sterling (Jun 07 2021 at 12:37):David Michael Roberts said:
The citation to "Sterling"/[Ste21] (made me chuckle) on the last slide on the univalent version: is that available/soon available/just over the next rise?
I hope very soon ;-) It's my thesis.
David Michael Roberts (Jun 07 2021 at 12:50):I suspected so. Good luck!
Tom Hirschowitz (Jun 08 2021 at 06:46):Here's a naive question. Why do you consider as a renaming, as opposed to a proper substitution? I'm not challenging the result, just trying to follow the intuitions.
Jon Sterling (Jun 08 2021 at 18:00):The reason we need it to be a "renaming" (I realize this term no longer makes sense) is that in the model, we need the interval to be tiny --- i.e. exponentiation by the interval needs to preserve colimits. If you don't include the face maps in the base category, this won't work out.
Tom Hirschowitz (Jun 09 2021 at 08:52):I see, thanks.
Jon Sterling (Sep 13 2021 at 21:44):Update: I successfully defended my dissertation today!!
Valeria de Paiva (Sep 13 2021 at 21:52):Congrats!
Jade Master (Sep 18 2021 at 17:08):Congrats Jon, I know I'm late to the party
Jon Sterling (Sep 18 2021 at 19:41):Thanks everyone ! :)
Jon Sterling (Sep 23 2021 at 15:33):Hi all, my defense video is available on YouTube here: https://www.youtube.com/watch?v=_4D97I8qYJw
Jon Sterling (Sep 28 2021 at 07:10):Happy to announce that the draft of Yue Niu, myself, Harrison Grodin and Bob Harper on a cost-aware logical framework has been conditionally accepted to POPL '22.
Preprint: https://arxiv.org/abs/2107.04663
Agda formalization: http://www.jonmsterling.com/agda-calf/index.html
In this work, we use the internal language of Artin gluings (which I call "synthetic Tait computability") to develop a logical framework in which you can verify both the input-output behavior of functional programs as well as their computational complexity.
Jon Sterling (Apr 22 2022 at 08:28):I'm now hosting a bibliography of Synthetic Tait Computability on my website here: https://www.jonmsterling.com/stc-bibliography.html. The goal is to bring visibility to all work using this technique, so please write to me if you have something that you want added to this page.
Valeria de Paiva (Apr 23 2022 at 22:01):and did you tell Bill about it? I think he might be interested. williamtait@mac.com
Jon Sterling (May 07 2022 at 14:13):I have also started to host a centralized bibliography of Guarded Domain Theory: https://www.jonmsterling.com/gdt-bibliography.html
Gershom (May 07 2022 at 20:15):Neat! Should Nakano's works be added there, or are they somehow not quite in the line of research as you see it? Same for McBride/Atkey I suppose. Perhaps they're about guarded recursion but not "domain theory" semantics of such?
Jon Sterling (May 07 2022 at 21:49):It's a very good question... It is hard to draw the line, but I think both the papers you mention ought to be in there --- because they were very influential for the development of guarded domain theory.
Gershom (May 08 2022 at 03:03):By the way let me mention that Nakano had a subsequent paper, the year following his paper that is always cited. It does two things I had wondered about -- it is the first one to introduce the term "later" for the modality, and it also shows a version of the system that is a conservative extension of the intuitionistic fragment of (finite?) GL provability logic. In reading some material on guarded domain theory, a related question that occurred to me is if some of the presheaf topos models can be shown to be categorifications of the classic kripke models of GL.
Jon Sterling (May 08 2022 at 21:43):Thanks @Gershom, I haven't read this second paper but now I think I should...