Superdeduction in Lambda-bar-mu-mu-tilde

Clement Houtmann (1)

1 PAREO - Formal islands: foundations and applications

Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on Christian Urban's work on classical sequent calculus. However Christian Urban's calculus is not directly related to the Curry-Howard correspondence contrarily to the lbmmt-calculus which relates straightaway to the lambda-calculus. This short paper is my first step towards a further exploration of the computational content of superdeduction proofs, for I extend the lbmmt-calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. I also prove strong normalisation for this extension of the blmmt-calculus.

Mots clés: Classical sequent calculus; Superdeduction; lambda-bar-mu-mu-tilde-calculus

Domaines: Logique en informatique [cs.LO]

Clement Houtmann. Superdeduction in Lambda-bar-mu-mu-tilde. Classical Logic and Computation 2010, Aug 2010, Brno, Czech Republic. pp.33-43, ⟨10.4204/EPTCS.47.5⟩. ⟨inria-00498744⟩