HighLevelProofsThatDontLeakLowLevelDetails

Speaker: Paul Brauner, Post-doctoral Fellow

I will present Superdeduction, a principle that allows for the integration of certain axiomatic theories in the sequent calculus. The benefits of doing so are several: proofs are usually more readable and more structured. Moreover, depending on the theory, proof normalization holds, enabling witness extraction within a theory. I will discuss whether a theory enables proof normalization or not and present some fun application of that framework: proof refactoring.

My most recent research page is : http://www.loria.fr/~brauner