Jesper Agdakx 🔸Sep 30
So I was going through the @icfp_conference papers of this year and I wanted to highlight a few that I thought are really cool. So here we go!

First up is "Type Theory in Type Theory using a Strictified Syntax" by Ambrus Kaposi and Loïc Pujet. Doing formal metatheory of type theory in type theory is notoriously hard but this paper tackles one of the key annoyances which is dealing with substitutions in a way that they commute with the syntax constructors. Even if you're not interested in the technical details, the introduction provides a very nice and approachable (*) overview of different approaches and the problems faced by each of them.

(*) except for the paragraph starting with "A short technical summary for category theorists", which I can only dream of understanding one day.

dl.acm.org/doi/10.1145/3747535

#TypeTheory #Agda
Show threadJesper Agdakx 🔸Sep 30
Second is "Robust Dynamic Embedding for Gradual Typing" by Koen Jacobs, Matías Toro, Nicolas Tabareau, and Éric Tanter. Just when you thought that the field of different criteria for gradual type systems had been fully explored, there is another one that is at the same time quite intuitive and not implied by any of the previous criteria. It's also fully formalized in Rocq (actually using Iris) which is quite impressive.

dl.acm.org/doi/10.1145/3747507

#GradualTyping #Rocq #Iris
Show threadJesper Agdakx 🔸Sep 30
Third up: the experience report "Teaching Software Specification" by Cameron Moy and Daniel Patterson. This paper makes the provocative but very good point that (at least) some courses on software verification could actually benefit by teaching formal *specification* instead. I found section 7 (interviews with students who took two very different versions of their course) particularly interesting. I just might have to make some changes to my FP course based on this.

(Also I was glad to see the work of @sarantja on teaching theorem provers getting a mention here!)

dl.acm.org/doi/10.1145/3747533

#SoftwareVerification #SoftwareSpecification #Education
Show threadJesper Agdakx 🔸Sep 30
For the category "most unexpected topic at ICFP" I give the award to "Polynomial-Time Program Equivalence for Machine Knitting" by Nathan Hurtig, Jenny Han Lin, Thomas S. Price, Adriana Schulz, James McCann, and Gilbert Louis Bernstein. It is a beautiful paper about giving a denotational semantics to algorithms for (yes) knitting machines and using it to prove correctness of optimizations. Also it has some very pretty pictures.

dl.acm.org/doi/10.1145/3747517

#MachineKnitting #FunctionalProgramming
Show threadJesper Agdakx 🔸Sep 30
Back to the usual suspects of ICFP, "McTT: A Verified Kernel for a Proof Assistant" by Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, and Brigitte Pientka describes a fully verified kernel for a proof assistant based on MLTT, complete with type checking, normalization, and extraction. I think the most exciting thing about this paper is the prospect of enabling easy development and experimentation with *domain-specific* type theories while having very strong guarantees about not breaking important meta-theoretic properties.

dl.acm.org/doi/10.1145/3747511

#TypeTheory #Rocq
Show threadJesper Agdakx 🔸
Finally, "First-Order Laziness" by Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley seems like a very useful contribution to the practical implementation of functional languages which could make them both more efficient and more friendly to the programmer by providing better debugging.

dl.acm.org/doi/10.1145/3747530

#FunctionalProgramming #LazyEvaluation
Sep 30 at 4:00pmWeb
Show threadJesper Agdakx 🔸Sep 30
Now probably I missed other papers that are equally exciting, so which ones are your favorites?
Show threadLindsey KuperSep 30
@jesper This one is kind of inside baseball, but I'm looking forward to "Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach" (https://dl.acm.org/doi/10.1145/3747510). It might shed some light on how to accomplish our (hand-wavy) goal of turning causal separation diagrams into a programming language that comes with a nice program logic.
Show threadLindsey KuperSep 30
@jesper And I too am looking forward to the machine knitting program equivalence paper, which is also sort of related to CSDs (where program equivalence is also going to be hairy). But I'm not really surprised by it -- it's exactly the paper that I hoped those folks would write! ❤️
Show threadLindsey KuperSep 30
@jesper And "Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages" (https://dl.acm.org/doi/10.1145/3747516) isn't related to anything I work on, but it sounds kind of like "we did static analysis to figure out when it's OK to use dynamic scope", which just sounds cool!