← Feed

Posts

• View post

  A message from my colleague Benedikt Ahrens: Hi all, I have funding for a postdoc position at TU Delft on combining computer proof assistants and computer algebra systems in the area of category theory, and I would be happy to hear from potential applicants before the formal advert goes out. I am looking for someone who is interested in all three of proof assistants, computer algebra systems, and category theory, and who has some experience in at least one or two of them. The position ideall...

• View post

  I'm back from a two week trip through Norway together with my parents! It was 15 years ago since I was there (except for TYPES in Oslo in 2019) but it was still as staggeringly beautiful as I remembered. I also had a lot of fun with the new fisheye lens I got for my good ol' Panasonic MFT camera. (in case your instance only supports 4 images per post, please view this post directly on agda.club for the rest) #Norway #Photography #LandscapePhotography #MicroFourThirds

• View post

  I regret to announce that as of today, I will cease all assisting activities, effective immediately. In other news, if you are in need of someone to associate with, please get in touch.

• View post

  The joys of booking European train tickets: travel from Delft to Rzeszow edition. Look up tickets on bahn.de: well 23h of uninterrupted trains seems excessive, how about we make a stop in Berlin?Actually I heard there’s a sleeper train to Berlin, let’s check it out!Oh the only place I can book it is in europeansleeper.eu, fine I guess.Sleeper train only goes on specific days of the week. Well there’s one on Friday, then we can stay one day+night in Berlin before continuing to Rzeszow, perfect!F...

• View post

  Heard at TYPES: FPW is definitely happening, and will be organized in Paris concurrently with ICFP. So if you are looking at the ICFP program and wondering what's up with the missing workshops, this is where you should go: irif.fr/~scherer/events/fpw-2026/announce.html

• View post

  This is your yearly reminder that for many people it is entirely possible to donate some percentage of their income - perhaps just 1% or perhaps even 10% - to good causes without changing much in their lifestyle. And if donated wisely, this can make a big positive difference in the lives of many people or animals, or help prevent some very bad things from happening. It's true that it won't solve any systemic issues and it won't release you from your duty to vote and advo...

• View post

  As part of our (@sarantja@mastodon.social and yt) research on the usability of interactive theorem provers, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in tools that encourage and facilitate type-driven development, especially in cases when they can help us reason about complex problems. We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven deve...

• View post

  Apparently the new diamond open access version of JFP is now up and running 🥳 jfp.episciences.org/ #JFP #FunctionalProgramming #OpenAccess

• View post

  I recently installed the Unhook browser plugin for Youtube (unhook.app/), and it *almost* turns it into something resembling a reasonable video platform. The main features: * Hide recommended videos to the side * Hide recommended videos at the end of a video * Hide shorts * Hide "trending videos" * Replace the home screen with my subscriptions Together with uBlock origin and SponsorBlock (which I already had installed) I can now actually (gasp) watch videos! I still wish more...

• View post

  I'm watching the documentary "From Gaza With Love", which is about the past two years in Gaza, with special attention to the lives of the children there. I've already seen a lot of videos, but still I'm absolutely speechless at the inconceivable contrast between the kids playing and laughing and the total destruction and suffering. It makes everything else I was worrying about suddenly feel tiny in comparison. You can watch the whole thing for free on Y...

• View post

  Our department is hiring an assistant professor in computer science (including programming languages). If you would like to join our small but diverse PL group in beautiful little Delft, please don't hesitate to apply! Also feel free to reach out to me if you want to know anything about our department or academic life in the Netherlands. Deadline for applications: 11th of May academictransfer.com/en/jobs/360114/assistant-professor-in-computer-science/ #TUDelft #AssistantProfessor #Hir...

• View post

  I'm very happy to announce that Andreea Costea is joining our PL group in Delft, starting in October 2024! You can find out about her work on her website: comp.nus.edu.sg/~andreeac/ Our group is also hiring a PhD student to work with Andreea on the topic Trustworthiness of Auto-Generated Systems. The deadline for applications is on **September 26** so don't wait too long to apply! All information about the application procedure is available here: tudelft.nl/over-tu-delft/werken...

• View post

  Fancy new name binding technique just dropped: arxiv.org/abs/2512.09464 (work by Antoine van Muylder, @anuytstt and Dominique Devriese). It includes such things as nominal pattern matching and synthetic Kripke parametricity. It's even implemented as an extension to "the mature proof assistant Agda"! [EDIT: actually it's only the older binary version that has been implemented, not this nullary version.] Disclaimer: I haven't read the paper yet, but this...