?. In and [. Kirchner-kirchner, Rusinowitch developed an Algebraic Logical Framework for first-order constrained deduction. Deduction rules and constraints are given for a first-order logic with equality. Enhancing LF K with constraints seems to be a perfect fit for a new race of metalanguages for proof checking and automatic theorem proving. Without going much into the details of our future research, the abstraction-term could, indeed, have the shape ? P x; C.M , where P records the first-order formula, x is a vector of variables occurring in the formula and C are constraints over x

?. Until, the predicate states a condition that takes as input the argument and its type It would be interesting to extend the framework with another predicate, say Q, applied to the body of the function. The abstraction would then have the form ? P x:A.M Q . This extension would put conditions on the function output, so leading naturally to a framework for defining Program LogicsàLogics

R. Avron, F. Honsell, M. Miculan, and C. Paravano, Encoding Modal Logics in Logical Frameworks, Studia Logica, vol.60, issue.1, pp.161-208, 1998.
DOI : 10.1023/A:1005060022386

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Pattern Type Systems, Proc. of POPL Hughes. A companion to Modal Logic. Methuen, pp.250-26195, 1984.

H. Cirstea, C. Kirchner, and L. Liquori, Matching Power, Proc. of RTA, pp.77-92, 2001.
DOI : 10.1007/3-540-45127-7_8
URL : https://hal.archives-ouvertes.fr/inria-00099308

H. Cirstea, C. Kirchner, and L. Liquori, The Rho Cube, Proc. of FOSSACS, pp.166-180, 2001.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

R. Harper, F. Honsell, and G. Plotkin, A Framework for Defining Logics Preliminary version in proc, Journal of the ACM, vol.4087, issue.1, pp.143-184, 1993.

F. Honsell, M. Lenisa, and L. Liquori, A Framework for Defining Logical Frameworks, Electronic Notes in Theoretical Computer Science, vol.172, pp.399-436, 1990.
DOI : 10.1016/j.entcs.2007.02.014
URL : https://hal.archives-ouvertes.fr/hal-01148312

A. Nanevski, F. Pfenning, and B. Pientka, Contextual Model Type Theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.

K. Watkins, I. Cervesato, F. Pfenning, and D. Walker, A Concurrent Logical Framework I: Judgments and Properties, 2002.