AST Lib request I have a Master's student who's interested in doing a static analysis project that involves translating C++ code to JavaScript and/or wasm. Does anyone have recommendations for sane AST libraries for C++ and/or JS which will make sense to someone algebraic-data-type-brained like […]

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 slides for Types and Topology (https://tdejong.com/mhe60) are all up on the website now (where available)! @MartinEscardo

☕️ 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 […]

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 […]

Would I be crazy for including this review in my Teaching Dossier as evidence that my lectures actually provide value to students?

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 […]

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 […]

~ 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 […]

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 […]

There are a lot of cursed computers things but this is the most cursed computers thing https://benjojo.co.uk/u/benjojo/h/h4N78m1PjXYsYfzkGV

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 […]

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 […]

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

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]

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 […]

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

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 […]

People always talk about the Oxford comma but nobody talks about the BibTeX 'and'

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 […]

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 […]

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!!"

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]

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 […]

Have I mentioned how much I like Nicole Mortillaro? Great article, includes quotes from @JohnBarentine (there were various good reasons why she didn't interview me for this one, but fortunately a lot of other astronomers besides me are really worried about Reflect Orbital's thoughtless plan) […]

Whenever I see "GenAI basically can do the work of a junior dev", I assume that those people are using junior devs very differently from me. To me, the value of a junior developer is maybe like 20% the code they write, and 80% is a down payment to a future where they no longer are a junior. I […]

Today's horrific discovery: apparently my email Spam filter was seeing the "CFP" in "ICFP" and putting anything related to ICFP in my junk folder...

In Natural Models, is the notion of "representable morphism" an existing motion for natural transformations? Or was it invented for natural models to capture the idea of context extension?

CwF question: democratic and set-theoretic models I'm wondering if people can help me with a CwF puzzle I've been muddling through. Suppose we've got some context-category C, and we identify context with closed types, so we have a functor F : C => Set, where we interpret F(Gamma) as "elements […]

I can't be at ICFP/OOPSLA, but if you're there and you're talking to someone who's looking for a PhD position in Programming Languages, or a Master's position with the potential of switch to PhD after a year, put in a good word for me. Especially interested in supervising students who: * Don't […]

It's becoming increasingly clear to me that Reflect Orbital's fucking stupid giant mirror satellite, with absolutely NOTHING useful to offer, which will cause countless safety issues, ecological disasters, and destroy the night sky, is going to launch. A bunch of astronomers and I have sent out […]

I've got two new MSc students going to PLMW and ICFPOOPSLA this year. I wish I could go myself, but if you see anyone with University of Regina on their nametag, be extra nice to them for me!

A great researcher I work with @carlysagan is looking for research funding or a remote position! It is really depressing how little funding is available to research the effects of satellite reentries... we REALLY need to get more scientists on this, because 1-5 Starlinks per day are reentering […]

My passion project (formalizing the basics of synthetic projective geometry in Lean) is now public on Github! https://github.com/PSchwahn/IncidenceGeometry Just finished the definition of the projective closure of an affine plane. Now on to proving that it satisfies the projective plane axioms...

I've gotten 2 emails from people on the prairies who were sharing photos of what they thought was the debris fall. They were both not (one was a starlink train, one was a sunset-illuminated contrail), but that's really ok, I appreciate that they shared. It gives me a lot of hope that I'm […]

I remember a book on topology (published or unpublished? maybe only online?) for which I can't find a reference or a link. Can you help? In any case, it is a book that has no proofs. The idea of the book is to create a sequence of lemmas, each of which is obvious, so that the diligent […]

The Canada Revenue Agency is doing a public consultation on automatic tax filing (which they should have implemented …several decades ago!). Fill it out and let the CRA know that it’s a good idea! […]

Is there a version of Yoneda for things other than Set? I'm particularly interested in things like (C^op => Poset), or even more specifically, (Poset^op => Poset)

I cannot. Just. No. Saying "but don't forget to follow your universities rules!" does absolve the authors of this book, published by Springer, of their responsibility

This week I gave a lecture series at the School on Logical Frameworks and Proof Systems Interoperability. I spoke about programming language techniques for proof assistants. The lecture slides and the reference implementations of a minimalist type theory are available at […]

Really missing having an "auto" tactic in Agda. The new proof search is really good at finding proofs, but when I'm dealing with bounded semilattices, which are like 5 levels deep in a tower of algebraic structures, the proofs it produces are really gnarly

What's the elevator pitch for natural models? Are they just more compact than the (equivalent) CwF presentation? Or is there something more that they help with?

Agda implicits question I'm wondering, is there a way to prevent an implicit from being implicitly introduced? For example, I'm trying to prove a bunch of goals of the type: ``` *≗* : (f g : PosetHomomorphism A B) → Set (a₁ ⊔ b₂) f ≗ g = ∀ {x} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x ``` from Categories […]

Is anyone familiar with papers/tutorials which treat Galois Connections as a category? E.g. objects are Posets and arrows are Galois connections.

Is there a fancy version of Pi, the way that the integral symbol is a fancy version of Sigma?

Writing a paper where the langugage is Gran, resisting the urge to make the version where I add W-types Gwan

PhD position with Benno van den Berg on the semantics of Homotopy Type Theory (esp. effective Kan fibrations) at the ILLC in Amsterdam! https://www.illc.uva.nl/NewsandEvents/News/Positions/newsitem/15777/PhD-Position-in-the-Semantics-of-Homotopy-Type-Theory Application deadline: 27 September […]

There is a program that will print "yes" if it will rain tomorrow, and "no" otherwise. Proof. Tomorrow it will either rain or not. If it does, the program that prints "yes" will do. Otherwise, take the program that prints "no". QED.