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
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
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
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 formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940. ,
DOI : 10.2307/2371199
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 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
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. ,
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
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
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
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