Logic & Programming

My PhD thesis has been approved for defense. You can find it here : http://tel.archives-ouvertes.fr/tel-00529021/en/

Chapter 1 gives a constructive version of a Henkin-style proof of Godel's completeness theorem. Chapter 2 introduces a notion of model similar to Kripke models using which one can give a normalization-by-evaluation style proof of completeness for classical logic. Chapter 3 does the same thing for intuitionistic logic (including disjunction and the existential). Finally, Chapter 4 presents an extension of intuitionistic logic with delimited control operators which still remains intuitionistic (preserves disjunction and existence properties) and can prove the Double Negation Shift and Markov's Principle.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net