Daniel Weller from the Vienna University of Technology will give a talk on 23 October. He will be visiting Tuesday afternoon and Wednesday. If you would like to meet with him, please send email to Dale.
Considering Proofs As Services
Daniel Weller, Vienna University of Technology
Tuesday, 23 Oct 2012, 15h, Saclay Salle Flajolet
In this talk, we present a planned project that will investigate particular uses of formal proofs that have, as far as I am aware, not been considered yet. We take the notion of “software as a service”, in which the result of the execution of code on some data is provided to a user (instead of the code itself), and consider how formal proofs can be used in such a situation. For example, if the code has a correctness proof, it can be used to construct a correctness proof of the result of the execution. If done naively, this proof contains the full correctness proof of the code. This naturally leads to the problem of elimination of information from a proof, which can be accomplished by cut-elimination.
One way to analyse this situation is to focus on the “non-propositional”, i.e. first- and higher-order, content of a proof. If time permits, in the second part of the talk we sketch an approach to the analysis of cut-elimination from that point of view by applying methods from the epsilon-calculus (due to David Hilbert) to expansion tree proofs (due to Dale Miller).
