Tomorrow is already the deadline for the third edition of #WITS, the Workshop on the Implementation of Type Systems, colocated with #POPL 2024 in London. The page limit is one page, but just a single-paragraph abstract with an interesting idea for a talk is also very welcome! In particular contributors to #Haskell #OCaml #Rust #Scala #Coq #Lean #Agda #Idris #Cedille #Arend #CoolTT and even #TypeScript are warmly invited to give a talk about their experiences with implementing type systems.
Call for papers: popl24.sigplan.org/home/wits-2024#Call-for-Participation
Submission link: wits24.hotcrp.com/
#CoolTT
Just attended a talk by Jon Sterling on cubical type theory implementations: redtt and cooltt. Throughout the talk the speaker kept saying how all this stuff is already supported by Cubical Agda. I guess it was a good choice to choose Agda as language of preference for working with constructive type theories.
Client Info
Server: https://mastodon.social
Version: 2025.04
Repository: https://github.com/cyevgeniy/lmst