🇨🇦 Joey Eremondi

Hi journalists! Before I start targeted emails to journalists I've talked to before, I'm just going to put this out here and see if it works:

Now that Reflect Orbital https://www.reflectorbital.com/ has officially filed to launch their first satellite, does anyone want to write an article about […]

@BoydStephenSmithJr Subtypes with quantities are dangerous and to my knowledge nobody has figured out the theory yet.

If I had to bet, I'd say quantity polymorphism was more likely to work than subtyping.

Summer Undergraduate Internship - Boosts Welcome!

Are you a senior undergrad, interested in Programming Languages? Do you want to visit Canada for a paid 12-week internship?

I have three MITACS projects which are looking for undergraduate interns to work on:

* Flexible Pattern Matching in […]

⚠️ “A tsunami watch has been issued for multiple parts of the B.C. coast after a large earthquake in the Pacific basin near Kamchatka, Russia, on Tuesday afternoon” #BC #Canada

https://www.cbc.ca/news/canada/british-columbia/tsunami-watch-july-29-1.7596997

@aram I personally like Moodle, but get the impression that's not a widely held opinion?

Alright, question, can you define quotients (or at least Propositional truncation) using funext alone? Maybe at a universe level one higher than the type you're quotienting?

I'm guessing you won't get all the nice properties like (|x| = |y| implies R x y). But it feels like there should be a […]

Is there a good/standard notation for ascribing a type on dependent pairs, when you want each type former to synthesize? Like in @mevenlennonbertrand 's BCIC.

Carleson's Theorem [1] is fully formalised in Lean!

https://github.com/fpvandoorn/carleson/pull/453

1] [https://en.wikipedia.org/wiki/Carleson's_theorem "Carleson's original proof is exceptionally hard to read, and although several authors have simplified the argument there are still no easy […]

Which year's PLMW videos should I recommend to an undergraduate interested in, but new to, PL?

what are the best freie software solutions for desktop publishing these days? is it still called “desktop publishing”?

shiny pdf output, many pages

@dimpase Yeah this was exactly my experience with Dr Gruyter. That and a copy editor who kept trying to correct domain specific terminology.

Nice that they do open access and special issues but was a hassle.

Screenshot of the abstract page of an arXiv article with identifier arXiv:2507.03413. The title is "Is it true that most sets are Sidon?" The abstract is the single word: "No."

Wow. Shortest abstract ever? I imagine the only shorter one is a question for a title and the abstract to be a single digit number answer
https://arxiv.org/abs/2507.03413

Press release time!

We found a trans-Neptunian Object (TNO) on a very cool orbit: 2020 VN40 orbits the sun exactly once in the same amount of time that Neptune orbits the sun exactly 10 times. It's really far from Neptune (and the rest of the planets), yet very strongly tied to Neptune due to […]

Agda 2.8.0 has been released.

It has a number of features that are going to make things much easier for our teaching to undergrads:

(1) Self-contained binaries are now distributed for all platforms. No more installation hassle. 🎉

This should also make things much easier for anybody who would […]

@chris__martin But it's not like it's a uniform distribution. The more interesting/novel the question you're asking, the lower the odds are of getting a correct answer. Doesn't mean it's useless, but it does mean that approaches from stochastic algorithms like "run this multiple times to compare […]

PLDI 2014 or 2024? Personal website of Patrick Lam

I made a thing. Programming Language Design and Implementation is a top conference in the field of programming languages. This page randomly picks paper titles from 2014 and 2024; can you tell which is which?

https://patricklam.ca/pldi-quiz/

Weird Computer Contest
A contest to see the strangest computer being used to read mastodon/the fediverse. The prize is a cool drawing from me just for you.

Rules:

1. Post a reply to show your device and why it is strange. Can mean hardware and software. A photo is better.
2. You can't go too […]

What's everyone's favorite tutorial on algebraic datatypes and pattern matching? Nothing fancy, no theory, nothing dependent, just "this is what will make sense to someone who has only ever seen C/Java/C++/Python/JS etc.".

Bonus points if it's creative commons and I can borrow the text (with […]

Alright, Agda/Dependent types proof design question:

I've got an Inductive-Recursive definition:

```
data Foo (X : Type) : Type
El : {X : Type} -> Foo X -> Type

data Foo X where
Special : Foo X
FooNat : Foo X
FooDep : (dom : Foo X) -> (El dom -> Foo X) -> Foo X
... -- a bunch of other […]

Anyone familiar with the new polarity annotations in Agda 2.8.0? I'm trying to figure out why this doesn't work:
```
record PosPair (@++ X : Set) (@++ Y : Set) : Set where
inductive
field
fst : X
snd : Y
```
What I'm trying to get at is how to encode a type like
```
data Tree : Type where
Leaf […]

For my next #compiler project, I want to write the optimization passes myself, but I don't want to deal with generating machine code for multiple platforms. So tell me #programminglanguages #plt #compilers fedi, what is an IR that I can target that has a non-optimizing compiler to machine code […]

The second student formalization project was a piece of classic algebra, the Artin Wedderburn theorem, which states that a simple left artinian ring is isomorphic to the ring of matrices over a division ring.

Job Petrovčič, Matevž Miščič and Maša Žaucer worked on it. (At first just one of them […]

The more I learn about atmospheric chemistry, the more terrified and angry I am about satellite companies' blatant lack of consideration for how their actions will harm the atmosphere. I hope this gets a lot of press. Great work by a whole team of scientists, including @astrokiwi.bsky.social! […]

Assistant Professor (Tenure-Track), Department of Computer Science The Department of Computer Science at the University of Regina invites applications for a tenure-track Assistant Professor in Cybersecurity or closely related area, starting January 1 or July 1, 2026.The successful candidate will join a vibrant department of highly motivated researchers and educators including several world-renowned experts and a group of recently recruited early career faculty members who are already making impacts in their respective fields.

My university is hiring an assistant professor in Cybersecurity: https://urcareers.uregina.ca/postings/19339

Welp, in case we needed even more things to worry about, apparently in 3 days we're going to stress-test Starlink's current orbital configuration with a severe geomagnetic storm. After running simulations of Starlink's orbital configuration, I am honestly quite worried about how this is going to […]

Anyone have recommendations for a good clock that chimes hourly (but is configurable to not go at night?)

It's one of those things that has a million things on Amazon and Wal-Mart marketplace but I don't know what's actually good/reliable.

@abnv Doom emacs

Hmm thinking I might be wrong about this one, each morphism is exponentiable in Pos if it is a Galois Connection, but I'm not sure it's exponentiable in the category of Galois connections

Category Theory question:

Has anyone come across a proof that, if you have a category whose objects are meet semilattices, and whose morphisms are Galois Connections between the underlying partial orders, that the resulting category is LCCC?

I found this reference ( […]

Widely covered MIT paper saying AI boosts worker productivity is, in fact, complete bullshit it turns out.

https://www.wsj.com/tech/ai/mit-says-it-no-longer-stands-behind-students-ai-research-paper-11434092?st=sF3Wvo&reflink=desktopwebshare_permalink