Max S. New @maxsnew@types.pl
- website
- http://maxsnew.com/
- pronouns
- he/him or they/them
PL theorist, Category practitioner
Joined Apr 2022
Most perverse feeling in academia is when you see a truly beautiful advance in your field and it makes you feel *bad* because you didn't do it first.
As someone who is terrible at writing, I have a lot of empathy for people that write bad textbooks
I personally enjoy drinking alcohol and international travel and in person conferences. All of the perks of my job are problematic 🙃
You can instantly sound more philosophical by upper-casing certain words when you share your Thoughts. This is the Old School version of the (TM) meme
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.
"Research impact beyond publications" man I'm barely to "research impact through publications"
Max S. New
boosted
Yep going through my yearly "try to learn differential geometry again" phase
Max S. New
boosted
Man I wish I were in a more topical research area (dermatology)
Max S. New
boosted
@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 |- => |=
All this "what is a type" discourse is very confusing to me. If I asked for a definition of object that includes objects of a category, objects of a multicategory, objects of an infinity category would I expect there to be a useful answer?
Love to logon to twitter.com daily and be scolded remotely by Shriram for being a bad teacher lol
Max S. New
boosted
@docaustinlim Want to cast types? There's just one good way to do it.
Max S. New
boosted
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.
Max S. New
boosted
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.
Max S. New
boosted
#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.
Max S. New
boosted
(\(\LaTeX\) test) Why is \(\bot\) used for bottom when clearly \(\omega\) looks more like a bottom?
Max S. New
boosted
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
- website
- http://maxsnew.com/
- pronouns
- he/him or they/them
PL theorist, Category practitioner
Joined Apr 2022
