4 papers
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…
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…
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…
Synthetic 1-Categories in Directed Type Theory
Thorsten Altenkirch, Jacob Neumann
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin…