Great summary, thanks! One clarification—we called it PrlConf intending to talk about proof assistants, but as our program came together, it turned out that mo

Great summary, thanks! One clarification—we called it PrlConf intending to talk about proof assistants, but as our program came together, it turned out that most of the talks were about category theory, type theory and denotational semantics. I think these things are even more interesting than proof assistants! I hope that we can find a way to put it back on somehow.