🇨🇦 Joey Eremondi
@joey.mathstodon.xyz.ap.brid.gy
PL Researcher. Assistant Professor at the University of Regina. 🇨🇦
Currently recruiting grad students - see https://eremondi.com/post/recruiting-grad-2024/ […]
[bridged from https://mathstodon.xyz/@joey on the fediverse by https://fed.brid.gy/ ]
Currently recruiting grad students - see https://eremondi.com/post/recruiting-grad-2024/ […]
[bridged from https://mathstodon.xyz/@joey on the fediverse by https://fed.brid.gy/ ]
Alright, crazy Racket question.
The one last shibboleth for LLM-generated plait code that it likes to use `match` instead of `type-case`.
So if I were to implement a `match` bomb, by redefining it as a macro which would give the most confusing error messages possible, what things could I do? […]
The one last shibboleth for LLM-generated plait code that it likes to use `match` instead of `type-case`.
So if I were to implement a `match` bomb, by redefining it as a macro which would give the most confusing error messages possible, what things could I do? […]
Original post on mathstodon.xyz
mathstodon.xyz
December 19, 2025 at 11:30 PM
Alright, crazy Racket question.
The one last shibboleth for LLM-generated plait code that it likes to use `match` instead of `type-case`.
So if I were to implement a `match` bomb, by redefining it as a macro which would give the most confusing error messages possible, what things could I do? […]
The one last shibboleth for LLM-generated plait code that it likes to use `match` instead of `type-case`.
So if I were to implement a `match` bomb, by redefining it as a macro which would give the most confusing error messages possible, what things could I do? […]
Reposted by 🇨🇦 Joey Eremondi
The slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)!
@MartinEscardo
@MartinEscardo
Types and Topology: A workshop in honour of Martín Escardó's 60th birthday
tdejong.com
December 18, 2025 at 5:28 PM
The slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)!
@MartinEscardo
@MartinEscardo
Reposted by 🇨🇦 Joey Eremondi
☕️ For the sixth time (!), we’re running our little ASPLOS workshop on hardware design languages/compilers/etc. Papers are just two pages! So easy! Please submit! #latte26 https://capra.cs.cornell.edu/latte26/
LATTE ’26
capra.cs.cornell.edu
December 11, 2025 at 6:39 PM
☕️ For the sixth time (!), we’re running our little ASPLOS workshop on hardware design languages/compilers/etc. Papers are just two pages! So easy! Please submit! #latte26 https://capra.cs.cornell.edu/latte26/
Alright, crazy idea. Is it possible to limit/redefine what copy/paste does for Dr. Racket in a plugin? To add a (small) barrier to copying code from ChatGPT and/or other students?
I already have my students install a "CS 350" plugin, so I can in theory use that to intercept paste.
Something […]
I already have my students install a "CS 350" plugin, so I can in theory use that to intercept paste.
Something […]
Original post on mathstodon.xyz
mathstodon.xyz
December 15, 2025 at 4:07 PM
Alright, crazy idea. Is it possible to limit/redefine what copy/paste does for Dr. Racket in a plugin? To add a (small) barrier to copying code from ChatGPT and/or other students?
I already have my students install a "CS 350" plugin, so I can in theory use that to intercept paste.
Something […]
I already have my students install a "CS 350" plugin, so I can in theory use that to intercept paste.
Something […]
Well, RIP my PL class, ChatGPT and Claude can now produce plait code that compiles.
I hate all of my options:
* Make the exams worth more (probably what I'll have to do)
* Record every editor keystroke to make sure they didn't just cut and paste (terrible for privacy and also probably […]
I hate all of my options:
* Make the exams worth more (probably what I'll have to do)
* Record every editor keystroke to make sure they didn't just cut and paste (terrible for privacy and also probably […]
Original post on mathstodon.xyz
mathstodon.xyz
December 12, 2025 at 9:13 PM
Well, RIP my PL class, ChatGPT and Claude can now produce plait code that compiles.
I hate all of my options:
* Make the exams worth more (probably what I'll have to do)
* Record every editor keystroke to make sure they didn't just cut and paste (terrible for privacy and also probably […]
I hate all of my options:
* Make the exams worth more (probably what I'll have to do)
* Record every editor keystroke to make sure they didn't just cut and paste (terrible for privacy and also probably […]
Would I be crazy for including this review in my Teaching Dossier as evidence that my lectures actually provide value to students?
December 11, 2025 at 6:36 PM
Would I be crazy for including this review in my Teaching Dossier as evidence that my lectures actually provide value to students?
Reposted by 🇨🇦 Joey Eremondi
I'm happy that my proposal for an introductory course on Homotopy Type Theory / Univalent Foundations at the European Summer School in Logic, Language and Information 2026 in Prague was accepted!
A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture […]
A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture […]
Original post on mathstodon.xyz
mathstodon.xyz
December 11, 2025 at 4:16 PM
I'm happy that my proposal for an introductory course on Homotopy Type Theory / Univalent Foundations at the European Summer School in Logic, Language and Information 2026 in Prague was accepted!
A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture […]
A great opportunity to make use of @egbertrijke's recently published book, @MartinEscardo's lecture […]
Reposted by 🇨🇦 Joey Eremondi
Here, Calibre, in one release, went from a tool readers can use to, well, read, to a tool that fundamentally views books as textureless content, no more than the information contained within them. Anything about presentation, form, perspective, voice, is irrelevant to that view. Books are no […]
Original post on wandering.shop
wandering.shop
December 6, 2025 at 6:53 AM
Here, Calibre, in one release, went from a tool readers can use to, well, read, to a tool that fundamentally views books as textureless content, no more than the information contained within them. Anything about presentation, form, perspective, voice, is irrelevant to that view. Books are no […]
Reposted by 🇨🇦 Joey Eremondi
~ Academic Positions in Formal Methods (postdoc, assistant prof., associate prof.) ~
The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! You'll work on the formalisation of computer science as part of a global initiative, CSLib, in […]
The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! You'll work on the formalisation of computer science as part of a global initiative, CSLib, in […]
Original post on mastodon.acm.org
mastodon.acm.org
November 11, 2025 at 2:42 PM
~ Academic Positions in Formal Methods (postdoc, assistant prof., associate prof.) ~
The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! You'll work on the formalisation of computer science as part of a global initiative, CSLib, in […]
The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! You'll work on the formalisation of computer science as part of a global initiative, CSLib, in […]
Reposted by 🇨🇦 Joey Eremondi
I sometimes see people describing resistance to LLM assisted coding as gatekeeping and I get that, software engineering culture is absolutely rife with gatekeeping, I quite literally dedicated dedicated my career to developer education because I want more people to have access to these […]
Original post on glasgow.social
glasgow.social
November 29, 2025 at 1:37 PM
I sometimes see people describing resistance to LLM assisted coding as gatekeeping and I get that, software engineering culture is absolutely rife with gatekeeping, I quite literally dedicated dedicated my career to developer education because I want more people to have access to these […]
Reposted by 🇨🇦 Joey Eremondi
There are a lot of cursed computers things but this is the most cursed computers thing
https://benjojo.co.uk/u/benjojo/h/h4N78m1PjXYsYfzkGV
https://benjojo.co.uk/u/benjojo/h/h4N78m1PjXYsYfzkGV
November 27, 2025 at 6:06 PM
There are a lot of cursed computers things but this is the most cursed computers thing
https://benjojo.co.uk/u/benjojo/h/h4N78m1PjXYsYfzkGV
https://benjojo.co.uk/u/benjojo/h/h4N78m1PjXYsYfzkGV
Reposted by 🇨🇦 Joey Eremondi
People (left leaning media figures) stop calling "grok" responding to something on X "fact checking" just because the LLM happened to be right one time *challenge*
Difficulty? Impossible??
Even if it's funny. eg. "Elon go FACT CHECKED by his own bot" yes that's funny but no facts were checked […]
Difficulty? Impossible??
Even if it's funny. eg. "Elon go FACT CHECKED by his own bot" yes that's funny but no facts were checked […]
Original post on sauropods.win
sauropods.win
November 26, 2025 at 6:40 PM
People (left leaning media figures) stop calling "grok" responding to something on X "fact checking" just because the LLM happened to be right one time *challenge*
Difficulty? Impossible??
Even if it's funny. eg. "Elon go FACT CHECKED by his own bot" yes that's funny but no facts were checked […]
Difficulty? Impossible??
Even if it's funny. eg. "Elon go FACT CHECKED by his own bot" yes that's funny but no facts were checked […]
Reposted by 🇨🇦 Joey Eremondi
Re: last boost https://chaos.social/@dpk/115589097803252590
That LLM-generated OCaml PR is a textbook illustration of open source in the era of vibe coding...
It's got everything:
- PR submitted without the author acknowledging they didn't write it and don't understand it.
- Copyright […]
That LLM-generated OCaml PR is a textbook illustration of open source in the era of vibe coding...
It's got everything:
- PR submitted without the author acknowledging they didn't write it and don't understand it.
- Copyright […]
Original post on aus.social
aus.social
November 22, 2025 at 1:06 AM
Re: last boost https://chaos.social/@dpk/115589097803252590
That LLM-generated OCaml PR is a textbook illustration of open source in the era of vibe coding...
It's got everything:
- PR submitted without the author acknowledging they didn't write it and don't understand it.
- Copyright […]
That LLM-generated OCaml PR is a textbook illustration of open source in the era of vibe coding...
It's got everything:
- PR submitted without the author acknowledging they didn't write it and don't understand it.
- Copyright […]
Reposted by 🇨🇦 Joey Eremondi
If you're new to x-box, you may find some of its buttons confusing, so I made this chart to help you figure it out
November 22, 2025 at 8:17 PM
If you're new to x-box, you may find some of its buttons confusing, so I made this chart to help you figure it out
Reposted by 🇨🇦 Joey Eremondi
After nine months of design, implementation, and orchestration, Lean's new module system I have been working on is now live in 4.26.0-rc1 and adopted throughout Mathlib. By introducing a system for checked and enforced API boundaries between files, it allows […]
[Original post on functional.cafe]
[Original post on functional.cafe]
November 19, 2025 at 1:39 PM
After nine months of design, implementation, and orchestration, Lean's new module system I have been working on is now live in 4.26.0-rc1 and adopted throughout Mathlib. By introducing a system for checked and enforced API boundaries between files, it allows […]
[Original post on functional.cafe]
[Original post on functional.cafe]
Reposted by 🇨🇦 Joey Eremondi
Scientists have discovered that it is possible to just do something, without making a podcast about it
November 9, 2025 at 11:56 PM
Scientists have discovered that it is possible to just do something, without making a podcast about it
Does anybody have an Agda encoding of IR types (like Dybjer-Setzer or something) that is marked as terminating using --cubical-compatible?
@fnf had a nice implementation that works with --with-K, but it doesn't work when you go to --cubical-compatible (presumably due to this […]
@fnf had a nice implementation that works with --with-K, but it doesn't work when you go to --cubical-compatible (presumably due to this […]
Original post on mathstodon.xyz
mathstodon.xyz
November 8, 2025 at 6:54 PM
Does anybody have an Agda encoding of IR types (like Dybjer-Setzer or something) that is marked as terminating using --cubical-compatible?
@fnf had a nice implementation that works with --with-K, but it doesn't work when you go to --cubical-compatible (presumably due to this […]
@fnf had a nice implementation that works with --with-K, but it doesn't work when you go to --cubical-compatible (presumably due to this […]
So apparently in Canada, the (notably not-in-power) Conservatives are trying to replicate the US's attack on academia: https://docs.google.com/forms/d/e/1FAIpQLSdaITz2IRZUTHJNvsdaOZqKIMSgduTw7znanDwF8jB0LpQP0g/viewform
November 3, 2025 at 6:57 PM
So apparently in Canada, the (notably not-in-power) Conservatives are trying to replicate the US's attack on academia: https://docs.google.com/forms/d/e/1FAIpQLSdaITz2IRZUTHJNvsdaOZqKIMSgduTw7znanDwF8jB0LpQP0g/viewform
Reposted by 🇨🇦 Joey Eremondi
Today is my day to smugly gloat about how I live in a province where we stay on standard time all year long, so I didn't have to change my clocks last night.
Tomorrow is my day to be very frustrated and apologize a lot as I miss all the meetings that have shifted because everyone else's time […]
Tomorrow is my day to be very frustrated and apologize a lot as I miss all the meetings that have shifted because everyone else's time […]
Original post on mastodon.social
mastodon.social
November 2, 2025 at 6:15 PM
Today is my day to smugly gloat about how I live in a province where we stay on standard time all year long, so I didn't have to change my clocks last night.
Tomorrow is my day to be very frustrated and apologize a lot as I miss all the meetings that have shifted because everyone else's time […]
Tomorrow is my day to be very frustrated and apologize a lot as I miss all the meetings that have shifted because everyone else's time […]
Reposted by 🇨🇦 Joey Eremondi
People always talk about the Oxford comma but nobody talks about the BibTeX 'and'
November 2, 2025 at 3:28 PM
People always talk about the Oxford comma but nobody talks about the BibTeX 'and'
Reposted by 🇨🇦 Joey Eremondi
So what are the best practices for representing type theories with term-indexed types inside Agda (or equivalent)? Some big inductive-recursive blob containing definitions of weakening and substitution, or is there a nice way to defer them? (I don't care about large elimination or universes – at […]
Original post on mathstodon.xyz
mathstodon.xyz
November 1, 2025 at 9:46 AM
So what are the best practices for representing type theories with term-indexed types inside Agda (or equivalent)? Some big inductive-recursive blob containing definitions of weakening and substitution, or is there a nice way to defer them? (I don't care about large elimination or universes – at […]
Reposted by 🇨🇦 Joey Eremondi
In this thread, I'd like to (re)advertise my MGS'2019 lecture notes "Introduction to Univalent Foundations of Mathematics with Agda"
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents
In the lengthy Introduction, I explain how univalent foundations differ […]
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents
In the lengthy Introduction, I explain how univalent foundations differ […]
Original post on mathstodon.xyz
mathstodon.xyz
November 1, 2025 at 6:29 PM
In this thread, I'd like to (re)advertise my MGS'2019 lecture notes "Introduction to Univalent Foundations of Mathematics with Agda"
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents
In the lengthy Introduction, I explain how univalent foundations differ […]
https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#contents
In the lengthy Introduction, I explain how univalent foundations differ […]
Reposted by 🇨🇦 Joey Eremondi
Any music theory nerds on here?
In particular I would love to understand how my guitar and piano work and how composition works but honestly I will take recs for anything music related that made you go "wow that's cool!!"
In particular I would love to understand how my guitar and piano work and how composition works but honestly I will take recs for anything music related that made you go "wow that's cool!!"
October 29, 2025 at 9:07 PM
Any music theory nerds on here?
In particular I would love to understand how my guitar and piano work and how composition works but honestly I will take recs for anything music related that made you go "wow that's cool!!"
In particular I would love to understand how my guitar and piano work and how composition works but honestly I will take recs for anything music related that made you go "wow that's cool!!"
Reposted by 🇨🇦 Joey Eremondi
I'm in a #github internal group for high-profile FOSS projects (due to @leaflet having a few kilo-stars), and the second most-wanted feature is "plz allow us to disable copilot reviews", with the most-wanted feature being "plz allow us to block issues/PRs […]
[Original post on mastodon.social]
[Original post on mastodon.social]
October 24, 2025 at 4:17 PM
I'm in a #github internal group for high-profile FOSS projects (due to @leaflet having a few kilo-stars), and the second most-wanted feature is "plz allow us to disable copilot reviews", with the most-wanted feature being "plz allow us to block issues/PRs […]
[Original post on mastodon.social]
[Original post on mastodon.social]
From a (spam) prospective student this morning:
> My principal research is web developer, database management systems, human-computer interaction, computer architecture, theory, artificial intelligence, compilers, algorithms, software engineering, natural language processing, senior Python […]
> My principal research is web developer, database management systems, human-computer interaction, computer architecture, theory, artificial intelligence, compilers, algorithms, software engineering, natural language processing, senior Python […]
Original post on mathstodon.xyz
mathstodon.xyz
October 23, 2025 at 4:20 PM
From a (spam) prospective student this morning:
> My principal research is web developer, database management systems, human-computer interaction, computer architecture, theory, artificial intelligence, compilers, algorithms, software engineering, natural language processing, senior Python […]
> My principal research is web developer, database management systems, human-computer interaction, computer architecture, theory, artificial intelligence, compilers, algorithms, software engineering, natural language processing, senior Python […]