Using Typed Lambda Calculus to Implement Formal Systems on a Machine, Journal of Automated Reasoning, vol.9, pp.309-354, 1992. ,
Mechanized Metatheory for the Masses: The POPLmark Challenge, Theorem Proving in Higher Order Logics: 18th International Conference (LNCS), pp.50-65, 2005. ,
Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, pp.1-89, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102709
The Locally Nameless Representation, Journal of Automated Reasoning, pp.1-46, 2011. ,
Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence, Logic Programming, 20th International Conference, vol.3132, pp.269-283, 2004. ,
Higher Level Meta Programming in Qu-Prolog 3: 0, Logic Programming, Proceedings of the Eigth International Conference, pp.285-298, 1991. ,
Proof Theoretic Approach to Specification Languages, Ph.D. Dissertation. University of Pennsylvania, 1995. ,
Parametric higher-order abstract syntax for mechanized semantics, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.143-156, 2008. ,
A Formulation of the Simple Theory of Types, J. of Symbolic Logic, vol.5, pp.56-68, 1940. ,
Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with an Application to the Church-Rosser Theorem, Indagationes Mathematicae, vol.34, pp.381-392, 1972. ,
Higher-order abstract syntax in Coq, Second International Conference on Typed Lambda Calculi and Applications, pp.124-138, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00074124
ELPI: Fast, Embeddable, ?Prolog Interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015. ,
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2-A Survey, J. of Automated Reasoning, vol.55, pp.307-372, 2015. ,
Programs Using Syntax with First-Class Binders, Proceedings of the 26th European Symposium on Programming, vol.10201, pp.504-529, 2017. ,
A new approach to abstract syntax involving binders, 14th Symp. on Logic in Computer Science, pp.214-224, 1999. ,
A Framework for Specifying, Prototyping, and Reasoning about Computational Systems, 2009. ,
Combining generic judgments with recursive definitions, 23th Symp. on Logic in Computer Science, F. Pfenning, pp.33-44, 2008. ,
Nominal abstraction, Information and Computation, vol.209, pp.48-73, 2011. ,
Computing with relations, functions, and bindings, 2019. ,
, Try MLTS Online, 2018.
A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion, International Workshop on Higher Order Logic Theorem Proving and its Applications, vol.780, pp.414-426, 1994. ,
Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol.78, 1979. ,
Introduction to the HOL System, Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, pp.2-3, 1991. ,
A Framework for Defining Logics, J. ACM, vol.40, pp.143-184, 1993. ,
HOL Light: an overview, International Conference on Theorem Proving in Higher Order Logics, pp.60-66, 2009. ,
A Unification Algorithm for Typed ?-Calculus, Theoretical Computer Science, vol.1, pp.27-57, 1975. ,
Natural Semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science (LNCS), vol.247, pp.22-39, 1987. ,
URL : https://hal.archives-ouvertes.fr/inria-00075953
A Universe of Binding and Computation, Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), pp.123-134, 2009. ,
Functional pearl: I am not a number -I am a free variable, Proceedings of the ACM SIGPLAN Workshop on Haskell, 2004. ,
, , pp.1-9
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, J. of Logic and Computation, vol.1, pp.497-536, 1991. ,
Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, p.90011, 1992. ,
Forum: A Multiple-Conclusion Specification Logic, Theoretical Computer Science, vol.165, issue.96, p.45, 1996. ,
Bindings, mobility of bindings, and the ?-quantifier, 18th International Conference on Computer Science Logic (CSL) 2004 (LNCS), vol.3210, 2004. ,
Mechanized Metatheory Revisited, Journal of Automated Reasoning, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01884210
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
, Foundational Aspects of Syntax. Comput. Surveys, vol.31, 1999.
A proof theory for generic judgments, ACM Trans. on Computational Logic, vol.6, pp.749-783, 2005. ,
An Overview of ?Prolog, Fifth International Logic Programming Conference, pp.810-827, 1988. ,
Functional Unification of Higher-Order Patterns, 8th Symp. on Logic in Computer Science, pp.64-74, 1993. ,
, , 2018.
The Foundation of a Generic Theorem Prover, Journal of Automated Reasoning, vol.5, pp.363-397, 1989. ,
Isabelle: A Generic Theorem Prover, Number 828 in LNCS, 1994. ,
Higher-Order Abstract Syntax, Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp.199-208, 1988. ,
System Description: Twelf -A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger, pp.202-206, 1999. ,
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010. ,
Nominal Logic, A First Order Theory of Names and Binding, Information and Computation, vol.186, pp.165-193, 2003. ,
A Metalanguage for Programming with Bound Names Modulo Renaming, Mathematics of Program Construction. 5th International Conference, vol.1837, pp.230-255, 2000. ,
Practical programming with higher-order encodings and dependent types, Proceedings of the European Symposium on Programming, 2008. ,
System Description: Delphin -A Functional Programming Language for Deductive Systems, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, vol.228, pp.113-120, 2008. ,
An Overview of C? ml, Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005) (Electr. Notes Theor, vol.148, pp.27-52, 2006. ,
Static name control for FreshML, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS, pp.356-365, 2007. ,
The Teyjus System -Version 2, 2015. ,
? -calculus, internal mobility and agent-passing calculi, Theoretical Computer Science, vol.167, pp.235-274, 1996. ,
The nablacalculus. Functional Programming with Higher-order Encodings, Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA'05, 2005. ,
, The Seventeen Provers of the World (LNCS), Freek Wiedijk, vol.3600, pp.151-157
Outline of a Mathematical Theory of Computation, Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems. Princeton University, pp.169-176, 1970. ,
FreshML: Programming with Binders Made Simple, Eighth ACM SIGPLAN International Conference on Functional Programming, pp.263-274, 2003. ,
Reasoning about Higher-Order Relational Specifications, Proceedings of the 15th International Symposium on Princples and Practice of Declarative Programming, pp.157-168, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00787126