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

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

H. P. 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, POPL'03, pp.250-261

C. Battel and A. Felty, A Higher-Order Logical Framework for Reasoning about Programming Languages, Proc. of CMS Winter Meeting, 2015.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, PxTP 2012, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert et al., Experience with embedding hardware description languages in HOL, TPCD, pp.129-156, 1992.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, 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, Theorem Proving in Higher Order Logics, pp.201-216, 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, 1997.

J. Filliâtre, One Logic to Use Them All, Proc. of CADE 24 -the 24th International Conference on Automated Deduction, Lake Placid, 2013.
DOI : 10.1007/978-3-642-38574-2_1

F. B. Fitch, Symbolic Logic, An Introduction, American Journal of Physics, vol.21, issue.3, 1952.
DOI : 10.1119/1.1933410

D. Garg and M. C. Tschantz, From indexed lax logic to intuitionistic logic, 2008.

J. Girard, Light linear logic Information and Computation, pp.175-204, 1998.

R. Harper and D. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.613-67310, 2007.
DOI : 10.1006/inco.2001.2951

D. Hirschkoff, Bisimulation proofs for the ?-calculus in the Calculus of Constructions, TPHOL'97, n. 1275 in LNCS, pp.10-1007, 1997.

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

F. Honsell, M. Lenisa, and L. Liquori, A Framework for Defining Logical Frameworks Volume in Honor of G, pp.399-436, 2007.

F. Honsell, M. Lenisa, L. Liquori, and P. , Maksimovic, I. Scagnetto. An open logical framework. Accepted for publication in Journal of Logic and Computation, 2013.

F. Honsell, L. Liquori, and I. Scagnetto, L ax F: Side Conditions and External Evidence as Monads, MFCS 2014, Part I, v. 8634 of LNCS, pp.327-33910, 2014.
DOI : 10.1007/978-3-662-44522-8_28

F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto, Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks, Proc. of LFMTP 2015, pp.3-17, 2015.
DOI : 10.4204/EPTCS.185.1
URL : https://hal.archives-ouvertes.fr/hal-01170029

F. Honsell and . Wherefore, Semantics of Computation?, Proc. of HaPoC 2015 : 3rd International CONFERENCE on the HISTORY and PHILOSOPHY of COMPUTING, pp.8-11

F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto, LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads Accepted for publication in the Special Issue of Logical Methods in Computer Science devoted to Festschrift for Pierre-Louis Curien, 2016.

M. Kerber, A Dynamic Poincar?? Principle, Proc. of Mathematical Knowledge Management -5th International Conference, pp.44-53, 2006.
DOI : 10.1007/11812289_5

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

E. Moggi, The partial lambda calculus, 1988.

. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23
DOI : 10.1109/LICS.1989.39155
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787

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, CADE, v. 1632 of LNCS, pp.202-20610, 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
DOI : 10.1145/1389449.1389469
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8383

B. Pientka and J. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), IJCAR 2010, v. 6173 of LNCS, pp.15-21978
DOI : 10.1007/978-3-642-14203-1_2

D. Prawitz, Natural Deduction. A Proof Theoretical Study, Almqvist Wiksell, pp.978-0486446554, 1965.

A. Schack-nielsen and C. Schürmann, Celf ??? A Logical Framework for Deductive and Concurrent Systems (System Description), pp.320-326, 2008.
DOI : 10.1007/978-3-540-71070-7_28

P. Schroeder-heister, Paradoxes and Structural Rules Insolubles and consequences : essays in honor of Stephen Read, pp.203-211

P. Schroeder-heister, Proof-Theoretic Semantics, Self-Contradiction, and the Format of Deductive Reasoning, Topoi, vol.36, issue.1, pp.77-8510, 2012.
DOI : 10.1007/s11245-012-9119-x

A. Stump, Proof Checking Technology for Satisfiability Modulo Theories, Electronic Notes in Theoretical Computer Science, vol.228, pp.121-133, 2008.
DOI : 10.1016/j.entcs.2008.12.121

A. Stump, A. Reynolds, C. Tinelli, A. Laugesen, H. Eades et al., LFSC for SMT Proofs: Work in Progress, Proceedings of the 2nd International Workshop on Proof eXchange for Theorem Proving (PxTP'12), 2012.

Y. Wang and K. Chaudhuri, A Proof-theoretic Characterization of Independence in Type Theory, 13th International Conference on Typed Lambda Calculi and Applications, pp.332-346, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01222743

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