RSVP Here
Issuing Citations is public-facing event series aimed at fostering research connections, nurturing inchoate projects, and providing an organizational catalyst for future conferences and publications. It's a space for graduate students and early career faculty alike to co-present, interact, and form connections across disciplinary lines.
March’s event will feature one talk!
-
The field of proof theory discusses what makes a valid proof. It sits at the intersection of philosophy and mathematics. The field of type theory discusses how to categorize different constructs in a programming language. It sits at the intersection of computer science and, again, mathematics. It was gradually discovered in the last century that, in some rigorous sense, a proof of a statement is the same as a program of a type; proof theory and type theory are two lenses on the same concepts.
We will discuss a translation from one formal language to another, viewing both the source language and the target language through both these two lenses. I will share a nice proof-theoretic property of this translation, and briefly mention a nice computational property it has.
Beatrice Institute will provide apps and the first round of drinks for attendees, after which interlocutors are on their own.
Tip your bartenders, chase the rabbit, and see you on Thursday, January 15th!