K. Do?en, Abstract, Bulletin of Symbolic Logic, vol.53, issue.04, pp.477-503, 2003.
DOI : 10.2307/3072340

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, Computer Science Logic, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, 1992.
DOI : 10.1007/3-540-54487-9_58

M. Fiore, R. D. Cosmo, and V. Balat, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.35-50, 2006.
DOI : 10.1016/j.apal.2005.09.001
URL : https://hal.archives-ouvertes.fr/hal-00149560

N. Stanley, K. A. Burris, and . Yeats, The saga of the high school identities, Algebra Universalis, vol.52, pp.325-342, 2004.

D. Ilik, Axioms and decidability for type isomorphism in the presence of sums, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.1-53, 2014.
DOI : 10.1145/2603088.2603115
URL : https://hal.archives-ouvertes.fr/hal-00991147

G. Harold and H. , Orders of Infinity. The 'Infinitärcalcül' of Paul Du Bois-Reymond. Cambridge Tracts in Mathematics and Mathematical Physics, 1910.

D. Ilik, A compact representation of terms and extensional equality at the exp-log normal form of types, 2015.

D. Ilik, Delimited control operators prove Double-negation Shift, Annals of Pure and Applied Logic, vol.163, issue.11, pp.1549-1559, 2012.
DOI : 10.1016/j.apal.2011.12.008
URL : https://hal.archives-ouvertes.fr/hal-00647389

R. Dyckhoff and S. Negri, Abstract, The Journal of Symbolic Logic, vol.94, issue.04, pp.1499-1518, 2000.
DOI : 10.1007/BF01627506

D. Prawitz, Ideas and Results in Proof Theory, Proceedings of the Second Scandinavian Logic Symposium of Studies in Logic and the Foundations of Mathematics, pp.235-307, 1971.
DOI : 10.1016/S0049-237X(08)70849-8

J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, 2007.
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441254

N. Guenot and L. Straßburger, Symmetric normalisation for intuitionistic logic, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.45-46, 2014.
DOI : 10.1145/2603088.2603160
URL : https://hal.archives-ouvertes.fr/hal-01092105

J. Hudelmaier, -Space Decision Procedure for Intuitionistic Propositional Logic, Journal of Logic and Computation, vol.3, issue.1, pp.63-75, 1993.
DOI : 10.1093/logcom/3.1.63

M. Grigorii-efroimovich, Solvability of the problem of deducibility in LJ for a class of formulas which do not contain negative occurrences of quantors, Proceedings of the Steklov Institute of Mathematics, pp.135-145, 1968.

D. Leivant, Implicational complexity in intuitionistic arithmetic, The Journal of Symbolic Logic, vol.344, issue.02, 1981.
DOI : 10.1007/BF01977642

W. Burr, Abstract, The Journal of Symbolic Logic, vol.63, issue.03, pp.1223-1240, 2000.
DOI : 10.2307/2586698

J. Fleischmann, Syntactic Preservation Theorems for Intuitionistic Predicate Logic, Notre Dame Journal of Formal Logic, vol.51, issue.2, p.2010
DOI : 10.1215/00294527-2010-014

A. Schubert, K. Pawe-l-urzyczyn, and . Zdanowski, On the Mints Hierarchy in First-Order Intuitionistic Logic, Foundations of Software Science and Computation Structures, pp.451-465, 2015.
DOI : 10.1007/978-3-662-46678-0_29

M. Bezem and T. Coquand, Automating Coherent Logic, Logic for Programming, Artificial Intelligence, and Reasoning, pp.246-260, 2005.
DOI : 10.1007/11591191_18