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

D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.
DOI : 10.1145/2071368.2071370

URL : http://www.lix.polytechnique.fr/~dbaelde/productions/pool/mumall_draft_long.pdf

D. Baelde and K. Chaudhuri, Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

K. Chaudhuri, L. Lima, and G. Reis, Formalized Meta-Theory of Sequent Calculi for Substructural Logics, Electronic Notes in Theoretical Computer Science, vol.332, 2016.
DOI : 10.1016/j.entcs.2017.04.005

URL : https://doi.org/10.1016/j.entcs.2017.04.005

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

A. Gacek, D. Miller-&-gopalan, and . Nadathur, Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004

URL : https://doi.org/10.1016/j.ic.2010.09.004

A. Gacek, D. Miller-&-gopalan, and . Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-008-9097-2

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

U. Gérard and &. Miller, Separating Functional Computation from Relations, Valentin Goranko & Mads Dam 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), LIPIcs 82, pp.1-23, 2017.

C. Liang and &. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

URL : https://doi.org/10.1016/j.tcs.2009.07.041

M. Southern and &. Chaudhuri, A Two-Level Logic Approach to Reasoning about Typed Specification Languages, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs) 29, Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.557-569, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091544

Y. Wang, K. Chaudhuri, A. Gacek, and &. Nadathur, Reasoning about higher-order relational specifications, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.157-168, 2013.
DOI : 10.1145/2505879.2505889

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

B. Ziliani and &. Sozeau, A unification algorithm for Coq featuring universe polymorphism and overloading, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp.179-191, 2015.
DOI : 10.1145/2784731.2784751

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