2 papers
cs.PL2026
Fuss-free cumulative universes: theory and practice
Raphaël Sterbac, Jonathan Sterling
Universes are central to dependent type theory, and they are notoriously difficult to handle in a way that is both correct and usable. We propose a new "fuss-free" generalised alge…
cs.PL2026
Bidirectional Elaborators à la Carte
Andrew Slattery, Jonathan Sterling
Surface syntax in proof assistants like Rocq, Lean, Agda, and Idris is highly implicit, lacking many details that are needed for user-written code to denote precisely defined mathe…