, The Abella Prover Available at http://abella-prover.org, 2012.
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
Parametric higher-order abstract syntax for mechanized semantics, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.143-15610, 2008. ,
, Programming in Prolog, 1987.
Higher-order abstract syntax in Coq, Second International Conference on Typed Lambda Calculi and Applications, pp.124-138, 1995. ,
DOI : 10.1007/BFb0014049
URL : https://hal.archives-ouvertes.fr/inria-00074124
Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011. ,
DOI : 10.1016/j.ic.2010.09.004
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. ,
Functional programming with ? -tree syntax: Draft. Available from https, 2018. ,
TryMLTS. https://trymlts.github.io, 2018. ,
Semantical analysis of higher-order abstract syntax, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.204-213, 1999. ,
DOI : 10.1109/LICS.1999.782616
The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964. ,
DOI : 10.1093/comjnl/6.4.308
An Extension to ML to Handle Bound Variables in Data Structures: Preliminary Report, Proceedings of the Logical Frameworks BRA Workshop, pp.323-335, 1990. ,
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991. ,
DOI : 10.1093/logcom/1.4.497
Bindings, mobility of bindings, and the ?-quantifier, 18th International Conference on Computer Science Logic (CSL) 2004, p.24, 2004. ,
Programming with Higher-Order Logic, pp.10-1017, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, pp.1-49, 2008. ,
DOI : 10.1145/1352582.1352591
Programming in Martin-Löf's type theory : an introduction, International Series of Monographs on Computer Science, 1990. ,
, OCaml, 2018.
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010. ,
DOI : 10.1007/978-3-642-14203-1_2