, Logic programming with focusing proofs in linear logic, J. of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.

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

D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conf. on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

D. Baelde and D. Miller, Least and Greatest Fixed Points in Linear Logic, International Conference on Logic for Programming and Automated Reasoning (LPAR), pp.92-106, 2007.
DOI : 10.1007/978-3-540-75560-9_9

C. Baier and J. Katoen, Principles of model checking, 2008.

Z. Chihani, D. Miller, and F. Renaud, A Semantic Framework for Proof Evidence, Journal of Automated Reasoning, vol.42, issue.1, pp.287-330, 2017.
DOI : 10.1017/CBO9781139168717
URL : https://hal.archives-ouvertes.fr/hal-01390912

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

K. L. Clark, Negation as Failure, Logic and Data Bases, pp.293-322, 1978.
DOI : 10.1007/978-1-4684-3384-5_11

O. Delande, D. Miller, and A. Saurin, Proof and refutation in MALL as a game, Annals of Pure and Applied Logic, vol.161, issue.5, pp.654-672, 2010.
DOI : 10.1016/j.apal.2009.07.017
URL : https://hal.archives-ouvertes.fr/hal-00527922

E. A. Emerson, The beginning of model checking: A personal perspective Years of Model Checking -History, Achievements, Perspectives, Lecture Notes in Computer Science, vol.5000, pp.25-27, 2008.

A. Gacek, D. Miller, and G. Nadathur, Combining Generic Judgments with Recursive Definitions, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.33-44, 2008.
DOI : 10.1109/LICS.2008.33

A. Gacek, D. Miller, and G. Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-008-9097-2
URL : https://hal.archives-ouvertes.fr/hal-00776208

G. Gentzen, Investigations into logical deduction The Collected Papers of Gerhard Gentzen, pp.68-131, 1935.

G. Gentzen, New version of the consistency proof for elementary number theory, pp.252-286, 1938.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, Towards a geometry of interaction, In Categories in Computer Science Contemporary Mathematics, vol.92, pp.69-108, 1987.
DOI : 10.1090/conm/092/1003197

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Girard, A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs, 1992.

Q. Heath and D. Miller, A framework for proof certificates in finite state exploration, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp.11-26, 2015.
DOI : 10.1109/LICS.1993.287585
URL : https://hal.archives-ouvertes.fr/hal-01240172

M. I. Kanovich, Petri nets, Horn programs, Linear Logic and vector games, Annals of Pure and Applied Logic, vol.75, issue.1-2, pp.107-135, 1995.
DOI : 10.1016/0168-0072(94)00060-G
URL : https://doi.org/10.1016/0168-0072(94)00060-g

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
URL : https://doi.org/10.1016/j.tcs.2009.07.041

Z. Manna and A. Pnueli, Temporal verification of reactive systems: safety, 2012.
DOI : 10.1007/978-1-4612-4222-2

R. Mcdowell and D. Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, issue.1-2, pp.91-119, 2000.
DOI : 10.1016/S0304-3975(99)00171-1

R. Mcdowell and D. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002.
DOI : 10.1145/504077.504080

R. Mcdowell, D. Miller, and C. Palamidessi, Encoding transition systems in sequent calculus, Theoretical Computer Science, vol.294, issue.3, pp.411-437, 2003.
DOI : 10.1016/S0304-3975(01)00168-2

D. Miller, Foundational proof certificates, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, LFMTP '13, pp.150-163, 2015.
DOI : 10.1145/2503887.2503894
URL : https://hal.archives-ouvertes.fr/hal-01239733

D. Miller and V. Nigam, Incorporating Tables into Proofs, Computer Science Logic Lecture Notes in Computer Science, vol.4646, pp.466-480, 2007.
DOI : 10.1007/978-3-540-74915-8_35
URL : http://www.lix.polytechnique.fr/~nigam/docs/CSL07.pdf

D. Miller and A. Saurin, A Game Semantics for Proof Search: Preliminary Results, Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in Electronic Notes in Theoretical Computer Science, pp.543-563, 2006.
DOI : 10.1016/j.entcs.2005.11.072
URL : https://hal.archives-ouvertes.fr/hal-00527881

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic, vol.6, issue.4, pp.749-783, 2005.
DOI : 10.1145/1094622.1094628
URL : http://www.cse.psu.edu/~dale/papers/nabla-subm.pdf

D. Miller and A. Tiu, Extracting Proofs from Tabled Proof Search, Third International Conference on Certified Programs and Proofs, number 8307 in Lecture Notes in Computer Science, pp.194-210, 2013.
DOI : 10.1007/978-3-319-03545-1_13
URL : https://hal.archives-ouvertes.fr/hal-00863561

R. Milner, Communication and Concurrency, 1989.

Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift et al., Efficient model checking using tabled resolution, Proceedings of the 9th International Conference on Computer Aided Verification (CAV97), number 1254 in Lecture Notes in Computer Science, pp.143-154, 1997.
DOI : 10.1007/3-540-63166-6_16

C. Ramakrishnan, Model checking with tabled logic programming, ALP News Letter, 2002.

D. Sangiorgi and R. Milner, The problem of ???weak bisimulation up to???, In CONCUR Lecture Notes in Computer Science, vol.630, pp.32-46, 1992.
DOI : 10.1007/BFb0084781

D. Sangiorgi and D. Walker, ?-Calculus: A Theory of Mobile Processes, 2001.

P. Schroeder-heister, Rules of definitional reflection, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.222-232, 1993.
DOI : 10.1109/LICS.1993.287585
URL : http://esslli2009.labri.fr/documents/LICS1993-d.pdf

H. Schwichtenberg, Proof Theory: Some Applications of Cut-Elimination, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pp.739-782, 1977.
DOI : 10.1016/S0049-237X(08)71124-8

A. Tiu and D. Miller, A Proof Search Specification of the ??-Calculus, 3rd Workshop on the Foundations of Global Ubiquitous Computing, pp.79-101, 2005.
DOI : 10.1016/j.entcs.2005.05.006
URL : https://doi.org/10.1016/j.entcs.2005.05.006

A. Tiu and D. Miller, Proof search specifications of bisimulation and modal logics for the ??-calculus, ACM Transactions on Computational Logic, vol.11, issue.2, p.2010
DOI : 10.1145/1656242.1656248
URL : http://www.lix.polytechnique.fr/~dale/papers/bisimdraft2.pdf

A. Tiu and A. Momigliano, Cut elimination for a logic with induction and co-induction, Journal of Applied Logic, vol.10, issue.4, pp.330-367, 2012.
DOI : 10.1016/j.jal.2012.07.007
URL : https://doi.org/10.1016/j.jal.2012.07.007

A. Tiu, G. Nadathur, and D. Miller, Mixing finite success and finite failure in an automated prover, Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05), pp.79-98, 2005.