Higher-Order Dynamic Pattern Unification for Dependent Types and Records, Typed Lambda Calculi and Applications, pp.10-26, 2011. ,
DOI : 10.1007/978-3-642-14203-1_2
The TPS theorem proving system, LNCS, vol.8, issue.230, pp.663-664, 1986. ,
Crafting a Proof Assistant, Types for Proofs and Programs, pp.18-32, 2006. ,
DOI : 10.1007/978-3-540-74464-1_2
Abella: A system for reasoning about relational specifications, J. of Formalized Reasoning, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102709
The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics, 1984. ,
THF0 ??? The Core of the TPTP Language for Higher-Order Logic, Automated Reasoning, pp.491-506, 2008. ,
DOI : 10.1007/978-3-540-71070-7_41
A Brief Overview of Agda ??? A Functional Language with Dependent Types, TPHOLs, pp.73-78, 2009. ,
DOI : 10.1007/978-3-540-87827-8_28
Satallax: An automatic higher-order prover, Automated Reasoning, pp.111-117, 2012. ,
A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, 1940. ,
DOI : 10.2307/2371199
Ellipsis and higher-order unification, Linguistics and Philosophy, vol.8, issue.1, pp.399-452, 1991. ,
DOI : 10.1007/BF00630923
Unification with extended patterns, Theoretical Computer Science, vol.206, issue.1-2, pp.1-50, 1998. ,
DOI : 10.1016/S0304-3975(97)00141-2
Unification of higher-order patterns in a simply typed lambdacalculus with finite products and terminal type, RTA 1996, pp.347-361 ,
The undecidability of the second-order unification problem, Theoretical Computer Science, vol.13, issue.2, pp.225-230, 1981. ,
DOI : 10.1016/0304-3975(81)90040-2
The undecidability of unification in third order logic, Information and Control, vol.22, issue.3, pp.257-267, 1973. ,
DOI : 10.1016/S0019-9958(73)90301-X
A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975. ,
DOI : 10.1016/0304-3975(75)90011-0
Proving and applying program transformations expressed with second-order patterns, Acta Informatica, vol.11, issue.1, pp.31-55, 1978. ,
DOI : 10.1007/BF00264598
Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002. ,
DOI : 10.1145/504077.504080
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
Some uses of higher-order logic in computational linguistics, Proceedings of the 24th annual meeting on Association for Computational Linguistics -, pp.247-255, 1986. ,
DOI : 10.3115/981131.981165
Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992. ,
DOI : 10.1016/0747-7171(92)90011-R
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, CADE, vol.16, pp.287-291, 1999. ,
DOI : 10.1007/3-540-48660-7_25
Functional unification of higher-order patterns, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.64-74, 1993. ,
DOI : 10.1109/LICS.1993.287599
Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, Number 2283 in LNCS, 2002. ,
Unification and anti-unification in the Calculus of Constructions 28 Frank Pfenning and Carsten Schürmann. System description: Twelf ? A meta-logical framework for deductive systems, 6th Symp. on Logic in Computer Science LNAI 1632, pp.74-85, 1991. ,
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), IJCAR, pp.15-21, 2010. ,
DOI : 10.1007/978-3-642-14203-1_2
The Teyjus system ? version 2, 2015. ,
The Seventeen Provers of the World, LNCS, vol.3600, pp.151-157, 2006. ,
Higher-order unification revisited: Complete sets of transformations, Journal of Symbolic Computation, vol.8, issue.1-2, pp.101-140, 1989. ,
DOI : 10.1016/S0747-7171(89)80023-9
An extension of L-lambda unification, 2002. ,
Linear unification of higher-order patterns, Proc. Coll. Trees in Algebra and Programming, 1993. ,
DOI : 10.1007/3-540-56610-4_78
The Leo-III project, Joint Automated Reasoning Workshop and Deduktionstreffen, p.38, 2014. ,
A unification algorithm for Coq featuring universe polymorphism and overloading, pp.179-191, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01248804