References

Proofs of cut elimination have took two different ways for a long time: syntac-tic cut reduction and proofs that this process terminates [Gir71,DW03], and semantic proofs of cut admissiblity [Her05,BH06,LDM05,Oka99]. Recent works [Dow06,DH12,BHH11,CH12] tend to show that some unity exist between two methods. The goal of this project is therefore to compare those two approaches, and more specifically, to force cut admissibility to generate proofs in normal form that are reducts of the original proofs via an adequate reduction relation. The main framework of interest of this internship will be Deduction Mod-ulo, that provides in particular a unified way to study axiomatic theories and axiomatic cuts. 2 Subject The internship will first focus on the study of the pair of theorems soundness/(cut-free) completeness, and on the computational content of such a cut admissibility proof. This can for instance be made through a formalization in a (construc-tive) proof-assistant of the propositional fragment, as did Hugo Herbelin for completeness with respect to Kripke structures. The next steps will depend on the interests an results of the candidate. That could be for instance: – carrying the initial proof (in sequent calculus, natural deduction,...) through soundness and completeness in order to make a formal link between the original proof and the cut-free proof obtained at the very end. This reminds the “categorical glueing ” of [AHS95]. – model transformations [TvD88] that go from Heyting algebras to (extensions of) Kripke structures, in order to compare this work to Normalization by Evaluation [Coq93]. This last step will take us into the world of proof normalization, while we have started by pure semantic proofs of cut admissibility.