P. Adhs01-thorsten-altenkirch, M. Dybjer, P. J. Hofmann, and . Scott, Normalization by evaluation for typed lambda calculus with coproducts, LICS, 2001.

B. Vincent-balat, R. D. Cosmo, and M. P. Fiore, Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums, POPL, 2004.

C. Bns10-taus-brock-nannestad and . Schürmann, Focused Natural Deduction, LPAR (Yogyakarta), 2010.
DOI : 10.1007/978-3-642-16242-8_12

C. Kaustuv-chaudhuri, S. Hetzl, and D. Miller, A Systematic Approach to Canonicity in the Classical Sequent Calculus, 21st EACSL Annual Conference on Computer Science Logic, 2012.

C. Kaustuv-chaudhuri, D. Miller, and A. Saurin, Canonical sequent proofs via multi-focusing, IFIP TCS, 2008.

N. Gha95 and . Ghani, Beta-eta equality for coproducts, Proceedings of TLCA'95, number 902 in Lecture Notes in Computer Science, 1995.

K. Neelakantan and R. Krishnaswami, Focusing on pattern matching, POPL, 2009.

L. Sam and L. , Extensional rewriting with sums MS07 Dale Miller and Alexis Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic, TLCA CSL, 2007.

A. Saurin, Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique), 2008.

S. Robert and J. Simmons, Structural focalization. CoRR, abs/1109, 2011.

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