A. Ahmad, D. R. Licata, and R. Harper, Deciding coproduct equality with focusing. Online draft, p.13, 2010.

T. Altenkirch and T. Uustalu, Normalization by evaluation for lambda -2, FLOPS, p.13, 2004.
DOI : 10.1007/978-3-540-24754-8_19

URL : http://www.cs.nott.ac.uk/~txa/publ/flops04.pdf

T. Altenkirch, P. Dybjer, M. Hofmann, and P. J. Scott, Normalization by evaluation for typed lambda calculus with coproducts, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, 2001.
DOI : 10.1109/LICS.2001.932506

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

V. Balat, R. D. Cosmo, and M. P. Fiore, Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, POPL, p.13, 2004.
DOI : 10.1145/964001.964007

URL : https://hal.archives-ouvertes.fr/hal-00149561

C. Böhm, Alcune proprieta delle forme normali nel k-calcolo, IAC Pubbl, vol.696119, issue.1, p.13, 1968.

K. Chaudhuri, D. Miller, and A. Saurin, Canonical Sequent Proofs via Multi-Focusing, IFIP TCS, 2007.
DOI : 10.1007/978-0-387-09680-3_26

URL : https://hal.archives-ouvertes.fr/hal-00527893

K. Chaudhuri, F. Pfenning, and G. Price, A logical characterization of forward and backward chaining in the inverse method, J. Autom. Reasoning, vol.40, issue.6, p.12, 2008.

K. Chaudhuri, S. Hetzl, and D. Miller, A Systematic Approach to Canonicity in the Classical Sequent Calculus, CSL, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00772396

P. Curien, M. Fiore, and G. Munch-maccagnoni, A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL, p.12
URL : https://hal.archives-ouvertes.fr/hal-01256092

J. Daniel, R. Dougherty, and . Subrahmanyam, Equality between functionals in the presence of coproducts, Information and Computation, vol.157, issue.2, p.12, 2000.

M. Fiore and A. Simpson, Lambda Definability with Sums via Grothendieck Logical Relations, TLCA, 1999.
DOI : 10.1007/3-540-48959-2_12

URL : http://www.cogs.susx.ac.uk/users/marcelo/papers/Types/glr.ps

H. Friedman, Equality between functionals, Logic Colloquium, 1975.
DOI : 10.1007/BFb0064870

N. Ghani, Beta-Eta Equality for Coproducts, TLCA, 1995.
DOI : 10.1007/bfb0014052

D. Ilik, The exp-log normal form of types and canonical terms for lambda calculus with sums

C. Liang and D. Miller, Focusing and polarization in intuitionistic logic. CoRR, arxiv:0708.2252, 2007.
DOI : 10.1007/978-3-540-74915-8_34

URL : https://hal.archives-ouvertes.fr/inria-00167231

S. Lindley, Extensional Rewriting with Sums, TLCA, 2007.
DOI : 10.1007/978-3-540-73228-0_19

URL : http://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf

G. Munch-maccagnoni and G. Scherer, Polarised Intermediate Representation of Lambda Calculus with Sums, 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science, p.12, 2015.
DOI : 10.1109/LICS.2015.22

URL : https://hal.archives-ouvertes.fr/hal-01160579

G. Scherer, Which types have a unique inhabitant? Focusing on pure program equivalence, 2016.
DOI : 10.1145/2784731.2784757

URL : https://hal.archives-ouvertes.fr/tel-01309712

G. Scherer and D. Rémy, Which simple types have a unique inhabitant, ICFP, 2015.
DOI : 10.1145/2784731.2784757

URL : https://hal.archives-ouvertes.fr/hal-01235596

R. J. Simmons, Structural focalization. CoRR, arxiv:1109, 2011.
DOI : 10.1145/2629678

A. Simpson, Categorical completeness results for the simply-typed lambda-calculus, TLCA, p.12, 1995.
DOI : 10.1007/BFb0014068

URL : http://www.dcs.ed.ac.uk/home/als/Research/completeness.ps.gz

R. Statman, Completeness, equivalence and lambda-definability, Journal of Symbolic Logic, vol.47, issue.1 1, 1982.
DOI : 10.2307/2273377

N. Zeilberger, The Logical Basis of Evaluation Order and Pattern- Matching, p.12, 2009.

N. Zeilberger, Polarity in proof theory and programming, 2013. URL http://noamz.org/talks/logpolpro.pdf. Lecture Notes for the Summer School on Linear Logic and Geometry of Interaction