H. Albert, TraktatüberTraktat¨Traktatüber kritische Vernunft, 1991.

N. Alechina, M. Mendler, V. De-paiva, and E. Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic, Proc. CSL'01, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21

P. Baillot, P. Coppola, and U. D. Lago, Light logics and optimal reduction: Completeness and complexity, Proc. LICS, pp.421-430, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00798315

H. Barendregt, Lambda Calculus: its Syntax and Semantics, 1984.

H. Barendregt and E. Barendsen, Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Pattern Type Systems, Proc. POPL'03, pp.250-261, 2003.

L. Carroll, What the Tortoise Said to Achilles. Mind, pp.278-280

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Proc. TLCA, v. 4583 of LNCS, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

M. Fairtlough, M. Mendler, and X. Cheng, Abstraction and Refinement in Higher Order Logic, Proc. TPHOL'01, number 2152 in LNCS, 2001.
DOI : 10.1007/3-540-44755-5_15

M. Fairtlough, M. Mendler, and M. Walton, First-order Lax Logic as a Framework for Constraint Logic Programming, Tech. Rep, 1997.

D. Garg and M. C. Tschantz, From indexed lax logic to intuitionistic logic, Tech. Rep., DTIC Document, 2008.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

D. Hirschko?, Bisimulation proofs for the ?-calculus in the Calculus of Constructions, Proc. TPHOL'97 number 1275 in LNCS, 1997.

F. Honsell and M. Lenisa, Semantical analysis of perpetual strategies in ??-calculus, Theoretical Computer Science, vol.212, issue.1-2, pp.183-209, 1999.
DOI : 10.1016/S0304-3975(98)00140-6

F. Honsell, M. Lenisa, and L. Liquori, A Framework for Defining Logical Frameworks. v. in Honor of G, pp.399-436, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01148312

F. Honsell, M. Lenisa, L. Liquori, and P. , Maksimovic, and I. Scagnetto. An Open Logical Framework, Journal of Logic and Computation, 2013.

F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto, A Conditional Logical Framework, Proc. LPAR'08, v. 5330 of LNCS, pp.143-157, 2008.
DOI : 10.1007/978-3-540-89439-1_10
URL : https://hal.archives-ouvertes.fr/hal-00909574

F. Honsell, M. Miculan, and I. Scagnetto, ??-calculus in (Co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2001.
DOI : 10.1016/S0304-3975(00)00095-5

M. Mendler, Constrained Proofs: A Logic for Dealing with Behavioural Constraints in Formal Hardware Verification, Proc. Designing Correct Circuits, pp.1-28, 1991.
DOI : 10.1007/978-1-4471-3544-9_1

E. Moggi, The partial lambda calculus, College of Science and Engineering. School of Informatics, 1988.

A. Nanevski, F. Pfenning, and B. Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.
DOI : 10.1145/1352582.1352591
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, Proc. CADE, v. 1632 of LNCS, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

B. Pientka and J. Dunfield, Programming with proofs and explicit contexts, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.163-173, 2008.
DOI : 10.1145/1389449.1389469

B. Pientka and J. Dunfield, Beluga: A framework for programming and reasoning with deductive systems (system description) Automated Reasoning, v. 6173 of LNCS, pp.15-21, 2010.

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