V. Breazu-tanen, D. Kesner, and L. , Puel: \A typed pattern calculus, IEEE Symposium on Logic in Computer Science, pp.262-274, 1993.

V. Danos, J. Joinet, and H. Schellinx, \LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication, Proceedings of the Workshop on Linear Logic, Cornell, 1993.

A. G. Dragalin, Mathematical Intuitionism: Introduction to Proof Theory, Translations of mathematical monographs, 1988.

J. Gallier, Constructive logics Part I: A tutorial on proof systems and typed ??-calculi, Theoretical Computer Science, vol.110, issue.2, pp.249-339, 1993.
DOI : 10.1016/0304-3975(93)90011-H

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol.59, issue.3, pp.201-217, 1993.
DOI : 10.1016/0168-0072(93)90093-S
URL : https://hal.archives-ouvertes.fr/inria-00075095

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

Z. Benaissa, D. Briaud, P. Lescanne, and J. , Rouyer-Degli, \, a calculus of explicit substitutions which preserves strong normalisation, 1995.

G. Pottinger, Normalization as a homomorphic image of cut-elimination, Annals of Mathematical Logic, vol.12, issue.3, pp.323-357, 1977.
DOI : 10.1016/S0003-4843(77)80004-1

D. Prawitz, Natural Deduction, a Proof-Theoretical Study, Almquist and Wiksell, pp.90-91, 1965.

W. A. Howard, \The Formulae-as-Types Notion of Constructions, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1969.

P. Wadler, \A Curry-Howard isomorphism for sequent calculus, 1993.