Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani +1
Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of comput…
cs.LO2025
Substitution Without Copy and Paste
Thorsten Altenkirch, Nathaniel Burke, Philip Wadler
Defining substitution for a language with binders like the simply typed -calculus requires repetition, defining substitution and renaming separately. To verify the categorical p…
cs.LO2024
Formalising Inductive and Coinductive Containers
Stefania Damato, Thorsten Altenkirch, Axel Ljungström
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed c…