iiinova — where your digital self keeps evolving

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 01/10/2026

Sending an email asking when a conference will start accepting submissions. Resisting the urge to make the subject line "ITP CFP ETA"

000

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 25/09/2026

Well, *someone* needs to post about this on Mastodon www.cbc.ca/news/canada/british-colu…

4868

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 24/09/2026

Does anybody have any nice Emacs commands/scripts for building/extending Agda equality reasoning proofs? I find them much easier to read, but a pain to type in.

000

Reposted by 🇨🇦 Joey Eremondi

Bastian Greshake Tzovaras @gedankenstuecke.scholar.social.ap.brid.gy · 23/09/2026

«They have mellowed out with age, but this fact remains engraved in their DNA: if no artists are stakeholders, you can’t produce a tool meant for artists. And given that they’re not purporting very hard to be making a tool for artists, it’s unfair to resent them for not making what they have not […]

scholar.social

Original post on scholar.social

001

Reposted by 🇨🇦 Joey Eremondi

Tamara Munzner @tamara.cosocial.ca.ap.brid.gy · 22/09/2026

We're hiring at UBC CS in our tenure-track teaching stream. We're in search of systems expertise: our greatest needs are in operating systems and computer architecture; also networking, distributed systems, database systems, cloud computing, and systems security […]

cosocial.ca

Original post on cosocial.ca

005

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 15/09/2026

RE: mathstodon.xyz/@joey/11705516034297… - Final Call - Applications are due Sep 16 at 1pm Pacific Time. Please apply, or forward this to undergrads you know who would be interested in applying.

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 14/09/2026

Is there a version of Agda's WellFounded induction which doesn't require FunExt to prove that it calculates an actual fixed point? Something like this, but without the f-ext premise: agda.github.io/agda-stdlib/v2.2/Ind…

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 10/09/2026

No funExt. No univalence. Just suffering.

100

Reposted by 🇨🇦 Joey Eremondi

Adrianna Tan @skinnylatte.hachyderm.io.ap.brid.gy · 10/09/2026

The year is 2026. Nobody wants a gamified experience on a website. Don’t give me a badge. Don’t even perceive me

2552

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 09/09/2026

Suppose, *hypothetically*, someone had a paper that was ideal for CPP, but wasn't likely to have it done in time for the deadline. Where would you recommend submitting? Bonus points if submissions open in the next couple months. Something that's very much "Here's a literate Agda file […]

mathstodon.xyz

Original post on mathstodon.xyz

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 08/09/2026

Anyone have tricks for embedding Agda in LaTex /without/ using Literate Agda? Is there any way for the LaTeX backend to generate a file of definitions that I can refer to by name to put a code snippet in LaTeX? Or a way to make a call to agda from LaTeX to do the highlighting? I don't want to […]

mathstodon.xyz

Original post on mathstodon.xyz

100

Reposted by 🇨🇦 Joey Eremondi

Sebastian Ullrich @kha.functional.cafe.ap.brid.gy · 02/09/2026

The real numbers are the friends we made along the way

012

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 31/08/2026

Degoogling, boosts welcome Has anyone used Typewire? Was interested because they're Canadian hosted, don't advertise any LLM stuff, and seem security focused. But I've never heard of them before today and for all I know they're full of crap.

100

Reposted by 🇨🇦 Joey Eremondi

Jean Abou Samra (new account) @jeanas.mathstodon.xyz.ap.brid.gy · 28/08/2026

I uploaded to my website some notes on descriptive set theory, adapted from lectures I followed last semester: jean.abou-samra.fr/notes/DST.pdf They are unfinished and not very much proofread, but I had to set myself a deadline for making a first version public, or it would just never […]

mathstodon.xyz

Original post on mathstodon.xyz

001

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 26/08/2026

Who's hiring functional programmers in 2026? I've got a recent graduate who has been doing really good work on error messages in dependent types, who's taken both my PLAI and PLFA classes. Sadly I haven't been at conferences for a while, so I don't know who's giving out shirts these days. Is […]

mathstodon.xyz

Original post on mathstodon.xyz

000

Reposted by 🇨🇦 Joey Eremondi

Matt Boyd @3psboyd.mastodon.social.ap.brid.gy · 25/08/2026

I saw a pretty major contributor to Rust projects making the case for LLMs being used in programming, and one of the things they liked is that you can ask it all the technical questions you want without feeling embarrassed, and what an indictment of the work culture of software engineering that is.

31247

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 25/08/2026

In the agda-stdlib, is there a version of Curry/Uncurry to convert between `(All P v)` for `(P : A -> Set)` and `(v : Vec A n)`, and `(Vec (Σ A P) n)`? I know it's basic induction but it also seems like something that would be there already.

200

Reposted by 🇨🇦 Joey Eremondi

Royce Williams @tychotithonus.infosec.exchange.ap.brid.gy · 22/08/2026

Having this printed out on the wall behind where I normally join calls, and being able to point to it when its bingo square comes up in discussion, continues to pay dividends, @mcc

Post from @mcc@mastodon.social:

According to our telemetry, 100% of our users have telemetry enabled

Aug 23, 2025,12:31 PM Tusky

04133

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 19/08/2026

Related to last toot, what's the precise sense that GATs and CwFs correspond? The barrier I'm having is that the types don't seem to mismatch: a specific GAT defines a theory, which will have a bunch of models. But CwFs are a specific theory. It's clear how the theory of CwFs is a GAT, but I […]

mathstodon.xyz

Original post on mathstodon.xyz

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 19/08/2026

Anyone have an Agda formalization of (the definition of) GATs lying around?

000

Reposted by 🇨🇦 Joey Eremondi

Anil Madhavapeddy @avsm.amok.recoil.org.ap.brid.gy · 19/08/2026

I'm delighted to announce that our formerly plain PDF ICFP 2026 paper (anil.recoil.org/papers/2026-package…) has been UPGRADED with advanced AI summaries (if you pay up for the premium ACM account) and is under impenetrable cybersecurity protection (if you click through […]

amok.recoil.org

Original post on amok.recoil.org

104

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 10/08/2026

[DarkSky donation link] I feel bad posting a donation link, because there are so very very many things worthy of donation. But, if you love the night sky, hate what Reflect Orbital and SpaceX are doing to it, and happen to have some spare cash, DarkSky International now has a fund specifically […]

mastodon.social

Original post on mastodon.social

1221

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 07/08/2026

Other than gradual typing, are there areas in type theory where we want types to be ordered or in some kind of lattice? Or even just pointed? I've got some stuff cooking and I'm trying to figure out if it's useful beyond the application to gradual types.

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 28/07/2026

Alright, suppose I want to mechanize some metatheory in Rocq. Nothing crazy, standard things like progress and preservation and confluence of some calculus. What's currently available for tools to manage definitions of syntax and capture-avoiding substitution, automatically derive the usual […]

mathstodon.xyz

Original post on mathstodon.xyz

000

Reposted by 🇨🇦 Joey Eremondi

Jef Poskanzer @jef.mastodon.social.ap.brid.gy · 27/07/2026

What does closure mean to you? I can think of at least three different things. At least I think they are different. - A function plus the environment is executes in. - A special operator in a regular expression, such as *. - A set containing all possible results of applying a function to another […]

mastodon.social

Original post on mastodon.social

100

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 13/07/2026

Related to previous question, do (postulated) quotients play nicely with IR, with respect to termination? E.g. I'm in a situation where the only thing I need funext for is showing that something is proof-irrelevant. So I can instead get rid of funext and just use a Squash type to make my […]

mathstodon.xyz

Original post on mathstodon.xyz

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 13/07/2026

Are there any papers that show MLTT is strongly normalizing if you add Induction Recursion and funext? Or at least "has no infinitely reducing terms". I realize that there isn't canonicity (since there are now non-refl equality proofs), and I'm assuming it's consistent, since the standard […]

mathstodon.xyz

Original post on mathstodon.xyz

100

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 11/07/2026

I'm doing Well Founded Induction in Agda, but in my hypothesis, I need a proof that the proof of y < x is irrelevant. Is there a way to do this without resorting to Cubical/Quotients?

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 05/07/2026

Are there any symbolic execution/static analysis/abstract interpretation tools for functional programs that are already implemented and runnable? Specifically that support HOFs and recursion. Obviously a heavy amount of conservative approximation will be necessary. I'm aware of some papers […]

mathstodon.xyz

Original post on mathstodon.xyz

212

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 03/07/2026

Sanity check... with ordinals (specifically Brouwer trees), you can't prove (∀ x . P (x)) from ∀ x . (P(x) ⟹ P(↑ x)), right? E.g. in the induction principle, you get P(y) for all (y < x), but the property I'm proving is of the form Q(Σ[ a ∈ A](size a ≤ x)), e.g. I'm proving a property of the […]

mathstodon.xyz

Original post on mathstodon.xyz

100

Reposted by 🇨🇦 Joey Eremondi

Zach Weinersmith @zachweinersmith.bsky.social · 27/06/2026

Something I worry about a little with this Ai art stuff is I only *think* I can spot it, but actually it's toupee fallacy: en.wiktionary.org/wiki/toupee_... Like, by definition, when Ai art doesn't look like Ai art, you don't notice.

en.wiktionary.org

toupee fallacy - Wiktionary, the free dictionary

712110

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 22/06/2026

Every exam I invigilate I like to live dangerously by googling "Big Clock" on a computer hooked up to the projector

000

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 22/06/2026

Currently sitting in on a Homotopy Colimit Summer school. I'm guessing it's mostly going to be beyond my background knowledge, but I'm wondering if any of these topics are likely to show up / be useful for dependent type stuff? - Model categories - Equivariant homotopy theory - Functor calculus […]

mathstodon.xyz

Original post on mathstodon.xyz

000

Reposted by 🇨🇦 Joey Eremondi

jonny (nonvenomous) @jonny.neuromatch.social.ap.brid.gy · 16/06/2026

RE: thepit.social/@peter/11676131756682… > In the observed case: 1.2M+ tokens consumed in ~30 minutes on a task that should have been git clone + find . -name '*.sol'. The recursive agent tree was still growing when observed. > > In another instance, this same pathological behavior […]

neuromatch.social

Original post on neuromatch.social

2019

Reposted by 🇨🇦 Joey Eremondi

dgelessus @dgelessus.mastodon.social.ap.brid.gy · 14/06/2026

they call it "cross compiling" because you will be very cross when trying to do it

11116

Reposted by 🇨🇦 Joey Eremondi

Tom de Jong @de-jong-tom.mathstodon.xyz.ap.brid.gy · 14/04/2026

I'm on the PC of Computer Science Logic (CSL 2027). csl2027.github.io The abstract/paper submission deadlines are 8/15 July 2026 (AoE) with notification of accepted papers on 15 October 2026, and the conference itself on 25-29 January 2027 in Brighton. I would love to see papers on […]

mathstodon.xyz

Original post on mathstodon.xyz

014

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 04/06/2026

Side rant: man I wish I could take a train across Canada instead of flying! But that's just not a viable option for so many reasons. Despite the name of the rail company being "VIA" SIGHHHH.

025

Reposted by 🇨🇦 Joey Eremondi

Adrian Sampson @adrian.discuss.systems.ap.brid.gy · 31/05/2026

seems insensitive of CACM to publicly post someone’s AI psychosis? cacm.acm.org/blogcacm/i-spent-a-yea…

It started almost by accident. At my startup Dwelly, I constantly push the limits of what AI tools can actually do. One day I just typed into a chat: “Can you prove P ≠ NP?”—referring to the problem the math community has been stuck on for decades.

Where I Am Now

I have a complete formalization of the P ≠ NP problem. All major publications have been analyzed and translated into code. I have an overall proof structure and a small number of clearly identified gaps: assumptions under which the problem is already solved. My current focus is turning those assumptions into proven statements.

029

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 29/05/2026

Im June, I'm starting a project with an undergrad student where we're cataloguing and evaluating different error messages in dependently typed languages. Right now, I'm planning to do Idris, Agda, Rocq and Lean. I'm wondering, what are the favorite exercise-based resources for each languages? […]

mathstodon.xyz

Original post on mathstodon.xyz

000

Reposted by 🇨🇦 Joey Eremondi

Prof. Sam Lawler @sundogplanets.mastodon.social.ap.brid.gy · 22/05/2026

YOU GUYS!! We live on a planet where the perfect combination of chemistry, atmospheric temperature and pressure, and geometry means that this ridiculously beautiful thing just HAPPENS sometimes!!! Earth is so damn neat! We have the best planet!

A ridiculously bright double rainbow in front of dark clouds. There are multiple supernumeraries (little tiny rainbows under the main rainbow). The colours are almost unreal they're so bright.

97682

Reposted by 🇨🇦 Joey Eremondi

Abhinav 🧭 @abnv.me · 20/03/2026

Friendship ended with `map`. Now `traverse` is my best friend. #Haskel #meme

050

Reposted by 🇨🇦 Joey Eremondi

kourge the jafnhár 🏳️‍🌈 @kourge.net · 12/05/2026

enough. i’m tired of github actions. it’s time for github consequences

302577665

🇨🇦 Joey Eremondi @joey.mathstodon.xyz.ap.brid.gy · 11/05/2026

What's the other 30%, Environment Canada?

A weather forecast showing a 70 Percent chance of rain or sun

100