A. Ahmad, D. R. Licata, and R. Harper, Deciding coproduct equality with focusing. Online draft, 2010. bi-intuitionistic validity, J. Autom. Reasoning, 2013.

N. Ghani, Beta-eta equality for coproducts, TLCA, 1995.

T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac, Complete completion using types and weights, PLDI, 2013.

H. Herbelin, A lambda-calculus structure isomorphic to gentzen-style sequent calculus structure, CSL, 1993.
URL : https://hal.archives-ouvertes.fr/inria-00381525

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
DOI : 10.1145/2603088.2603115
URL : https://hal.archives-ouvertes.fr/hal-00991147

E. Kmett and . Lens, URL https, 2012.

E. Kmett, Lens wiki ? types, 2013. URL https://github.com/ ekmett/lens

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

O. Laurent, A proof of the focalization property of linear logic, 2004.

C. Liang and D. Miller, Focusing and polarization in intuitionistic logic. CoRR, 2007.
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

P. López, F. Pfenning, J. Polakow, and K. Watkins, Monadic concurrent linear logic programming, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, 2005.
DOI : 10.1145/1069774.1069778

S. Mclaughlin and F. Pfenning, Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic, LPAR, 2008.
DOI : 10.1007/978-3-540-89439-1_12

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, CSL, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

C. D. Bruno and . Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects and implicits, OOPSLA, 2010.

C. D. Bruno, T. Oliveira, W. Schrijvers, W. Choi, K. Lee et al., The implicit calculus: A new foundation for generic programming, 2014.

M. Peter, S. Osera, and . Zdancewic, Type-and-example-directed program synthesis, PLDI, 2015.

J. Otten and C. Kreitz, A uniform proof procedure for classical and non-classical logics, In KI Advances in Artificial Intelligence, 1996.
DOI : 10.1007/3-540-61708-6_70

D. Perelman, S. Gulwani, T. Ball, and D. Grossman, Typedirected completion of partial expressions, PLDI, 2012.

G. Scherer, Mining opportunities for unique inhabitants in dependent programs, 2013.

G. Scherer, 2-or-more approximation for intuitionistic logic, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01094120

G. Scherer and D. Rémy, URL http://gallium.inria. fr, 2015.

R. J. Simmons, Structural Focalization, ACM Transactions on Computational Logic, vol.15, issue.3, 2011.
DOI : 10.1145/2629678

C. Stirling, Proof Systems for Retracts in Simply Typed Lambda Calculus, Automata, Languages, and Programming -ICALP, 2013.
DOI : 10.1007/978-3-642-39212-2_36

J. Peter, M. Stuckey, and . Sulzmann, A theory of overloading, ICFP, 2002.

N. Vorob-'ev, A new algorithm of derivability in a constructive calculus of statements, Problems of the constructive direction in mathematics, 1958.

P. Wadler and S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, 1989.
DOI : 10.1145/75277.75283

A. Lincoln and . Wallen, Automated proof search in non-classical logics: Efficient matrix proof methods for modal and intuitionistic logic, 1987.

J. B. Wells and B. Yakobowski, Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis, LOPSTR, 2004.
DOI : 10.1007/11506676_17

M. Zaoinc, Fixpoint technique for counting terms in typed lambdacalculus, 1995.

N. Zeilberger, Focusing and higher-order abstract syntax, POPL, 2008.