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

My paper "Continuous and algebraic domains in univalent foundations" with @MartinEscardo was accepted for publication by the Journal of Pure and Applied Algebra! 🎉
https://martinescardo.github.io/papers/continuous-algebraic-domains-in-uf.pdf

This paper has its origin in my very first paper with Martín (and my second paper overall) "Domain Theory in Constructive and Predicative Univalent Foundations" which appeared at Computer Science Logic (CSL) back in 2021.

Since then I wrote my PhD thesis on this topic (and worked on other things in type theory after) and the present paper is a revision of both the CLS'21 paper and my PhD thesis (which I completed in 2022).

Everything in the paper has been formalized and an HTML rendering of the Agda file that directly links the code to the paper can be found here: https://martinescardo.github.io/TypeTopology/DomainTheory.Continuous-and-algebraic-domains.html

#typetheory #agda #logic #math #computerscience

My paper "Continuous and algebraic domains in univalent foundations" with @MartinEscardo was accepted for publication by the Journal of Pure and Applied Algebra! 🎉
https://martinescardo.github.io/papers/continuous-algebraic-domains-in-uf.pdf

This paper has its origin in my very first paper with Martín (and my second paper overall) "Domain Theory in Constructive and Predicative Univalent Foundations" which appeared at Computer Science Logic (CSL) back in 2021.

Since then I wrote my PhD thesis on this topic (and worked on other things in type theory after) and the present paper is a revision of both the CLS'21 paper and my PhD thesis (which I completed in 2022).

Everything in the paper has been formalized and an HTML rendering of the Agda file that directly links the code to the paper can be found here: https://martinescardo.github.io/TypeTopology/DomainTheory.Continuous-and-algebraic-domains.html

#typetheory #agda #logic #math #computerscience