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, Computer Science Logic, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21

. Archimede and . Metodo, Nel laboratorio di un genio, Bollati Boringhieri, 2013.

A. Avron, F. Honsell, I. Mason, and R. Pollack, Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, vol.49, issue.3, pp.309-354, 1992.
DOI : 10.1007/BF00245294

A. Badiou, La relationénigmatiquerelationénigmatique entre philosophie et politique, Germina, 2011.

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

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, volume II, pp.118-310, 1992.

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

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

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, Typed Lambda Calculi and Applications, TLCA, 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.

F. B. Fitch, Symbolic logic, 1952.

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

J. Girard, The Blind Spot: lectures on logic, 2011.
DOI : 10.4171/088
URL : https://hal.archives-ouvertes.fr/hal-01322183

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Preliminary version in Proc. of LICS'87, pp.143-184, 1993.
DOI : 10.1145/138027.138060

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

D. Hirschkoff, 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, Electronic Notes in Theoretical Computer Science, vol.172, pp.399-436, 2007.
DOI : 10.1016/j.entcs.2007.02.014
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, LPAR'08, pp.143-157, 2008.
DOI : 10.1007/978-3-540-89439-1_10
URL : https://hal.archives-ouvertes.fr/hal-00909574

F. Honsell, L. Liquori, and I. Scagnetto, L ax F: Side Conditions and External Evidence as Monads, Proc. of MFCS 2014 (39th International Symposium on Mathematical Foundations of Computer Science), Part I, pp.327-339, 2014.
DOI : 10.1007/978-3-662-44522-8_28

F. Honsell and M. , ??-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, 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.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
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, Proc. of CADE, 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, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2

D. Prawitz, Natural Deduction. A Proof Theoretical Study, Almqvist Wiksell, 1965.

A. Schopenhauer, The World as Will and Representation, 1966.

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

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

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