J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

J. Andreoli, Focussing and proof construction, Annals of Pure and Applied Logic, vol.107, issue.1-3, pp.131-163, 2001.
DOI : 10.1016/S0168-0072(00)00032-4
URL : http://doi.org/10.1016/s0168-0072(00)00032-4

A. Asperti, W. Ricciotti, C. S. Coen, and E. Tassi, A compact kernel for the calculus of inductive constructions. S ¯ adhan ¯ a, pp.71-144, 2009.

D. Baelde, A linear approach to the proof-theory of least and greatest fixed points, 2008.

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr system for model checking over syntactic expressions Baelde and D. Miller. Least and greatest fixed points in linear logic, 21th Conference on Automated Deduction (CADE), number 4603 in LNAI International Conference on Logic for Programming and Automated Reasoning (LPAR), pp.391-397, 2007.

R. S. Boyer and J. S. Moore, A Computational Logic, 1979.

R. L. Constable, Implementing Mathematics with the Nuprl Proof Development System, 1986.

T. Coquand, G. G. Huet-]-n, ]. O. De-bruijn12, D. Delande, A. Miller et al., Influences of mathematical logic on computer science The Universal Turing Machine: A Half-Century Survey The mathematical language AUTOMATH, its usage, and some of its extensions Proof and refutation in MALL as a game Annals of Pure and Applied Logic Characterizing correctness properties of parallel programs using fixpoints The Conduct of Life On the unity of logic Locus solum: From the rules of logic to the logic of rules, Constructions: A Higher Order Proof System for Mechanizing Mathematics Symposium on Automatic Demonstration Proceedings of the 7th International Colloquium on Automata, Languages and Programming The Collected Papers of Gerhard Gentzen From LCF to HOL: a short history Proof, Language, and Interaction: Essays in Honour of Robin Milner20] J. Y. Halpern, R. Harper, N. Immerman, P. G. Kolaitis, M. Y. Vardi, and V. Vianu. On the unusual effectiveness of logic in computer science. Bulletin of Symbolic Logic, pp.151-184, 1969.

R. Kahle and P. Schroeder-heister, Introduction to proof theoretic semantics. Special issue of Synthese, 2006.
DOI : 10.1007/s11229-004-6292-5
URL : http://hdl.handle.net/10316/7627

M. Kulstad and L. Carlin, Leibniz´sLeibniz´s philosophy of mind The Stanford Encyclopedia of Philosophy, 2008.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

C. Liang and D. Miller, A Unified Sequent Calculus for Focused Proofs, 2009 24th Annual IEEE Symposium on Logic In Computer Science, pp.355-364, 2009.
DOI : 10.1109/LICS.2009.47

D. Miller, Proof theory as an alternative to model theory, Newsletter of the Association for Logic Programming, 1991.

D. Miller, A proof-theoretic approach to the static analysis of logic programs In Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, number 17 in Studies in Logic, pp.423-442, 2008.

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

D. Miller and V. Nigam, Incorporating Tables into Proofs, Computer Science Logic LNCS, vol.4646, pp.466-480, 2007.
DOI : 10.1007/978-3-540-74915-8_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.3026

R. A. Millo, R. J. Lipton, and A. J. Perlis, Social processes and proofs of theorems and programs. Communications of the Association of Computing Machinery, pp.271-280, 1979.

V. Nigam and D. Miller, Focusing in linear metalogic, Proceedings of IJCAR: International Joint Conference on Automated Reasoning, pp.507-522, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00281631

V. Nigam and D. Miller, Algorithmic specifications in linear logic with subexponentials, Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, PPDP '09, pp.129-140, 2009.
DOI : 10.1145/1599410.1599427

V. Nigam and D. Miller, A Framework for Proof Systems, Journal of Automated Reasoning, vol.40, issue.7, 2009.
DOI : 10.1007/s10817-010-9182-1

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.2627

L. C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, 1987.
DOI : 10.1017/CBO9780511526602

L. C. Paulson, J. Isabelle, J. Queille, and . Sifakis, The next 700 theorem provers Specification and verification of concurrent systems in CESAR A machine-oriented logic based on the resolution principle Revisiting the correspondence between cut elimination and normalisation, International Symposium on Programming, 5th Colloquium Proceedings ICALP: Annual International Colloquium on Automata, Languages and Programming Proceedings of the Conference on Logic of Programs, pp.361-386, 1965.