The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

The Agda standard library has been published in the Journal of Open Source Software. Congratulations to Matthew Daggitt, @gallais , James McKinna, Andreas Abel, @Taneb , @mudri , Ulf Norell, @oisdk, Sergei Meshveliani, Sandro Stucki, @JacquesC2, Alex Rice, Jason Hu, Li-yao Xia, Shu-Hung You, @totbwf and @wen !

joss.theoj.org/papers/10.21105/joss.09241

#Agda #ITP #DependentTypes #JOSS #OSS

Dependent types and how to get rid of them

https://chadnauseam.com/coding/pltd/are-dependent-types-actually-erased

#HackerNews #DependentTypes #Erasure #Coding #SoftwareDevelopment #Programming #LanguageTheory #HackerNews

"Why don't you use dependent types?"

https://lawrencecpaulson.github.io//2025/11/02/Why-not-dependent.html

#HackerNews #dependenttypes #programming #philosophy #typeTheory #HN #discussion #HackerNews

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers

Have you ever written Agda code in anger? Well now you can come and write Agda code in Angers!

The Agda Implementors’ Meeting XLI will take place in Angers, France from 2025-11-24 to 2025-11-29 (Mon to Sat). We have a very nice venue La Bulle en Bois which includes a coworking place, a vegan & organic canteen, and a fablab with 3d printers and laser cutters!

Registrations are now open on the Agda Wiki at https://wiki.portal.chalmers.se/agda/Main/AIMXLI and there is a soft registration deadline on 24 October. I hope to see many of you there!

#Agda#ProofAssistants#DependentTypes#Angers