Burak Ekici: Relative Hilbert-Post completeness for exceptions

Speaker: Burak Ekici, Université Joseph Fourier (Grenoble)

Abstract: A theory is complete if it does not contain a contradiction while all of its proper extensions do. In this talk, first I introduce a relative notion of syntactic completeness; then I prove that adding exceptions to a programming language can be done in such a way that the completeness of the language is not made worse. These proofs are formalized in a logical system which is close to the usual syntax for exceptions, and they have been checked with the proof assistant Coq.