Burak Ekici: Relative Hilbert-Post completeness for exceptions
Datum objave: 9. 11. 2015
Seminar za temelje matematike in teoretično računalništvo
Torek, 10. 11. 2015, od 12h do 14h, Plemljev seminar, Jadranska 19
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.