Getting around to listening to that Conal Elliott interview [1]. Talks about his love for denotational semantics but also wow his disdain for operational semantics. He expresses his belief that operational semantics is popular because it is easy to teach to grad students and churn out papers. I wouldn't word it so harshly but I've thought similar things. I like to say that the supremacy of operational semantics is the "worse is better" of academic PL. I invite the reader to appreciate this irony.
@dev papers should have a citation format where the first page of citations have the most "important" citations are on the right while the left column is just a list of funny anecdotes/bloopers. On the bottom part of that page is a future work section (i.e. post-credit scene) and only after that the less relevant citations start (with an appendix for extra post-credit stuff)
We had a similar discussion on the meaning of type soundness in M Felleisen's "history of programming languages" course. I took the radical but IMO only sensible position which was "whatever you say it means" or equivalently in pithy symbols |- => |=
@docaustinlim Want to cast types? There's just one good way to do it.
https://researchseminars.org/talk/ToposInstituteColloquium/57/
We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals. Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.
New ArXiV draft: Propositional Equality for Gradual Dependently Typed Programming
https://arxiv.org/abs/2205.01241
We show a language that lets you omit equality proofs, but remembers information about the values you equate, so it can raise an error when the equality can't possibly hold.
This lets you use dependent types as a unified interface for specifying statically and dynamically-checked assertions, and gives a principled semantics to programs with terms or types yet to be filled in.
I'm very happy to chat/ramble about it if people have questions.
Side-note: some of the math runs off the edge of the page. It doesn't do that when I build on my machine, so I'll have to figure out what ArXiV does different that's mucking it up.
#introduction
Hello, people on Mastodon! I'm new to this platform and still figuring things out.
My name is Yao Li (李垚). I am a researcher on programming languages/formal verification/interactive theorem proving. I am currently a Ph.D. candidate at Penn and an incoming assistant professor at Portland State University (Fall '22). Always happy to chat with people about research or general things about programming languages/functional programming/program verification.
announcement (boosts appreciated)
We're delighted to announce the HoTTEST Summer School, which will take place online everywhere in the world during the months of July and August 2022.
The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.
This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.
Read more: https://groups.google.com/g/homotopytypetheory/c/Ir2joc7imyI
Join the Discord: https://discord.gg/tkhJ9zCGs9
PL theorist, Category practitioner