My blog on everything Agda, dependent types, and life
Jesper Cockx - Introduction to Coinduction in Agda Part 1: Coinductive Programming Jesper Cockx Home Blog Papers Talks Teaching Links Introduction to Coinduction in Agda Part 1: Coinductive Programming Posted by Jesper on January 22, 2026 {-# OPTIONS --guardedness --sized-types #-} {-# OPTIONS --cubical -WnoUnsupportedIndexedMatch #-} {-# OPTIONS --allow-unsolved-metas #-} open import…
Jesper Cockx - Going Vegan, or How I Ran All Out Of Excuses Jesper Cockx Home Blog Papers Talks Teaching Links Going Vegan, or How I Ran All Out Of Excuses Posted by Jesper on January 3, 2026 It’s been clear to me for a while now that our diet can have a big impact on climate change. Up until 2019, I consequently called myself a “flexitarian” and tried to avoid eating meat as long as doing so was…
Jesper Cockx - The good places to submit your papers Jesper Cockx Home Blog Papers Talks Teaching Links The good places to submit your papers Posted by Jesper on December 19, 2025 This week, the ACM made the monumental(ly stupid) decision to replace the abstracts of papers on their Digital Library website by AI-written summaries. While this did not apply to all papers, and it was only visible to…
Jesper Cockx - Reflective journaling prompts Jesper Cockx Home Blog Papers Talks Teaching Links Reflective journaling prompts Posted by Jesper on September 15, 2024 This is a post about the practice of reflective journaling. I’m someone who likes to think about the world and myself and the relationship between the two, and writing down these thoughts makes them clearer and more concrete. However,…
Jesper Cockx - On erasure annotations and agda2hs Jesper Cockx Home Blog Papers Talks Teaching Links On erasure annotations and agda2hs Posted by Jesper on July 30, 2024 {-# OPTIONS --sized-types --erasure #-} module agda2hs-erasure where open import Haskell.Prelude open import Haskell.Law.Equality Name = String Var : @0 String → @0 List String → Set postulate _!?_ : List a → Int → Maybe a…
Jesper Cockx - Functional Programming in the Netherlands Jesper Cockx Home Blog Papers Talks Teaching Links Functional Programming in the Netherlands Posted by Jesper on July 17, 2024 Back in January of this year, I had the honor of hosting the `FP Dag’ – also known as the Dutch Functional Programming Day – here in Delft. Apart from several entertaining and thought-provoking talks, we also had a…
Jesper Cockx - A love letter to TTRPGs Jesper Cockx Home Blog Papers Talks Teaching Links A love letter to TTRPGs Posted by Jesper on June 30, 2024 While I mentioned my passion for tabletop role-playing games (TTRPGs) a few times before on this blog, I never dedicated a proper post to them. Let’s fix that! In their essence, tabletop role-playing games are a kind of game where you and a few friends…
Jesper Cockx - Agda Core: The Dream and the Reality Jesper Cockx Home Blog Papers Talks Teaching Links Agda Core: The Dream and the Reality Posted by Jesper on May 11, 2024 {-# OPTIONS --erasure #-} module agda-core where open import Haskell.Prelude --> One important purpose of a type system (and especially a dependent type system) is to increase the trustworthiness of the objects the types are…
Jesper Cockx - Ten Thinkers Who Shaped My Worldview Jesper Cockx Home Blog Papers Talks Teaching Links Ten Thinkers Who Shaped My Worldview Posted by Jesper on March 10, 2024 I believe it is our responsibility as world citizens to help building a better world and to protect those who cannot easily protect themselves. However, our world has become so complex and confusing that it is often not clear…
Jesper Cockx - 6 Reasons in favor of a core language, and 5 against Jesper Cockx Home Blog Papers Talks Teaching Links 6 Reasons in favor of a core language, and 5 against Posted by Jesper on February 10, 2024 As a person who has worked quite a bit on Agda, I sometimes get the question why Agda does not have a proper core language. And it’s a valid question, given that most - if not all - closely…
Jesper Cockx - Ten improvements to Agda's implementation Jesper Cockx Home Blog Papers Talks Teaching Links Ten improvements to Agda's implementation Posted by Jesper on January 1, 2024 Happy 2024! I have (foolishly) resolved to write one blog post per month in this new year, so expect more frequent and less polished posts in the coming year. To give myself a head start, here is the first of…
Jesper Cockx - An Invitation to Mindfulness Jesper Cockx Home Blog Papers Talks Teaching Links An Invitation to Mindfulness Posted by Jesper on September 24, 2023 If you are anything like me, you often crave for a bit of peace and clarity in your busy stressful life. Perhaps you often feel distracted by hundreds of things clamoring for your attention, and find it difficult to determine what is…
Jesper Cockx - Ten common writing issues in student papers Jesper Cockx Home Blog Papers Talks Teaching Links Ten common writing issues in student papers Posted by Jesper on August 1, 2023 Good writing is important, and it takes time to get it right. Over the last couple of months, I have been reading and giving feedback on way too many papers written by bachelor students, master students, PhD…
Jesper Cockx - I'm Autistic, and that's okay Jesper Cockx Home Blog Papers Talks Teaching Links I'm Autistic, and that's okay Posted by Jesper on April 22, 2023 I don’t expect this will be a surprise to people who know me, but at the same time I have never told most people. So I’m making it official now: I am Autistic (if you wonder about the capitalization of Autistic: please go read this post ).…
Jesper Cockx - Don't worry (about writing Haskell), be happy (writing Agda instead)! Jesper Cockx Home Blog Papers Talks Teaching Links Don't worry (about writing Haskell), be happy (writing Agda instead)! Posted by Jesper on October 4, 2022 {-# OPTIONS --sized-types --erasure #-} module agda2hs where open import Agda.Primitive using ( Level ) open import Relation.Binary.PropositionalEquality…
Jesper Cockx - 1001 Representations of Syntax with Binding Jesper Cockx Home Blog Papers Talks Teaching Links 1001 Representations of Syntax with Binding Posted by Jesper on November 4, 2021 As a compiler developer or programming language researcher, one very common question is how to represent the syntax of a programming language in order to interpret, compile, analyze, optimize, and/or transform…
Jesper Cockx - WITS '21: First International Workshop on the Implementation of Type Systems Jesper Cockx Home Blog Papers Talks Teaching Links WITS '21: First International Workshop on the Implementation of Type Systems Posted by Jesper on October 15, 2021 I am organizing the First International Workshop on the Implementation of Type Systems together with the one and only Richard Eisenberg. The…
Jesper Cockx - EuroProofNet: the European research network on digital proofs Jesper Cockx Home Blog Papers Talks Teaching Links EuroProofNet: the European research network on digital proofs Posted by Jesper on October 15, 2021 EuroProofNet is the European research network on digital proofs. It aims at boosting the interoperability and usability of proof systems. It gathers 190 researchers on proof…
Jesper Cockx - The Taming of the Rew Jesper Cockx Home Blog Papers Talks Teaching Links The Taming of the Rew Posted by Jesper on January 7, 2021 Back in 2019, I wrote two posts about user-definable rewrite rules in Agda (which have since then been rewritten into a TYPES paper ) and promised a third one about how to make rewrite rules safe to use (or at least safer ). At the time, I was hard at…
Jesper Cockx - Mijn uitdaging voor jou in 2021: Doe zoveel goed als je kan Jesper Cockx Home Blog Papers Talks Teaching Links Mijn uitdaging voor jou in 2021: Doe zoveel goed als je kan Posted by Jesper on December 24, 2020 (This post is also available in English .) Deze post is iets heel anders dan wat ik hier normaal schrijf. Deze keer wil ik het hebben over een idee waarvan ik echt geloof dat…
Jesper Cockx - My challenge for you in 2021: Do the most good you can Jesper Cockx Home Blog Papers Talks Teaching Links My challenge for you in 2021: Do the most good you can Posted by Jesper on December 24, 2020 (Deze post is ook vertaald naar het nederlands .) This post is quite different from the usual stuff I post here. It’s about an idea I believe is really important; not nearly enough…
Jesper Cockx - An introduction to property-based testing with QuickCheck Jesper Cockx Home Blog Papers Talks Teaching Links An introduction to property-based testing with QuickCheck Posted by Jesper on December 17, 2020 In February, I will be teaching a new course on Functional Programming at TU Delft. The course will mostly cover Haskell using Graham Hutton’s excellent book , though there will be…
Jesper Cockx - NWO Veni Grant on A Trustworthy and Extensible Core Language for Agda Jesper Cockx Home Blog Papers Talks Teaching Links NWO Veni Grant on A Trustworthy and Extensible Core Language for Agda Posted by Jesper on November 11, 2020 I’m very glad and humbled to announce that I received an NWO Veni Grant for my proposal “A Trustworthy and Extensible Core Language for Agda.” You can read…
Jesper Cockx - Announcement: I'm moving to Delft! Jesper Cockx Home Blog Papers Talks Teaching Links Announcement: I'm moving to Delft! Posted by Jesper on November 12, 2019 I’m very glad to announce that starting on the 1st of December, I will join the programming languages group at TU Delft as an assistant professor! Some of my new colleagues are Eelco Visser , Robert Krebbers , Casper Bach…
Jesper Cockx - Rewriting type theory Jesper Cockx Home Blog Papers Talks Teaching Links Rewriting type theory Posted by Jesper on October 30, 2019 MathJax is awesome! \[ \definecolor{AgdaComment}{rgb}{0.7,0.13,0.13} \definecolor{AgdaKeyword}{rgb}{0.8,0.4,0.0} \definecolor{AgdaNumber}{rgb}{0.63,0.13,0.94} \definecolor{AgdaCon}{rgb}{0.0,0.55,0.0} \definecolor{AgdaField}{rgb}{0.93,0.07,0.54}…
Jesper Cockx - Hack your type theory with rewrite rules Jesper Cockx Home Blog Papers Talks Teaching Links Hack your type theory with rewrite rules Posted by Jesper on October 21, 2019 This is the first in a series of three blog posts on rewrite rules in Agda. In contrast to my previous post , this post will decidedly non-introductory . Instead, we will have some fun by doing unsafe things and…
Jesper Cockx - Formalize all the things (in Agda) Jesper Cockx Home Blog Papers Talks Teaching Links Formalize all the things (in Agda) Posted by Jesper on October 4, 2019 I quite often hear from people that they are interested in learning Agda, and that’s great! However, I often feel there are not enough examples out there of how to use the different features of Agda to implement programs,…
Jesper Cockx - EUTYPES '19 Summer School in Ohrid Jesper Cockx Home Blog Papers Talks Teaching Links EUTYPES '19 Summer School in Ohrid Posted by Jesper on September 13, 2019 I gave a course about Correct-by-Construction Programming in Agda at the EUTYPES summer school in Ohrid. The course materials are available here . Site proudly generated by Hakyll
Jesper Cockx - Writing Agda blog posts in literate markdown Jesper Cockx Home Blog Papers Talks Teaching Links Writing Agda blog posts in literate markdown Posted by Jesper on July 9, 2019 So you got to admit all the cool kids are doing it nowadays: writing blog posts in literate Agda. Do you want to join the club? Then you’ve come to the right place! In this blog post I’ll explain how to write a…
Jesper Cockx - Elaborating Dependent (Co)pattern Matching Jesper Cockx Home Blog Papers Talks Teaching Links Elaborating Dependent (Co)pattern Matching Posted by Jesper on September 22, 2018 It has been a while since my last (and first) post, so here is a new one about this year’s ICFP paper by Andreas Abel and me, titled “Elaborating Dependent (Co)pattern Matching” ( pdf ). Dependent pattern…
Jesper Cockx - The Agda's New Sorts Jesper Cockx Home Blog Papers Talks Teaching Links The Agda's New Sorts Posted by Jesper on May 3, 2018 In the last few weeks, Sandro Stucki has given a couple of excellent presentations on pure type systems (pts’s) at the initial types club at Chalmers. Since I’ve been working on the implementation of Agda’s sorts system, and the new implementation is closely…