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

P. Brauner, C. Houtmann, and C. Kirchner, Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007.
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557

J. Brotherston and A. Simpson, Sequent calculi for induction and infinite descent, Journal of Logic and Computation, vol.21, issue.6, pp.1177-1216, 2011.
DOI : 10.1093/logcom/exq052

K. Chaudhuri, Subformula Linking as an Interaction Method, Proceedings of the 4th Conference on Interactive Theorem Proving (ITP), pp.386-401, 2013.
DOI : 10.1007/978-3-642-39634-2_28
URL : https://hal.archives-ouvertes.fr/hal-00937009

K. Chaudhuri, N. Guenot, and L. Straßburger, The Focused Calculus of Structures, Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, J. of Automated Reasoning, vol.31, issue.1, pp.31-72, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

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-011-9218-1
URL : https://hal.archives-ouvertes.fr/hal-00776208

N. Guenot, Nested Deduction in Logical Foundations for Computation, 2013.
URL : https://hal.archives-ouvertes.fr/pastel-00929908

A. Guglielmi, T. Gundersen, and M. Parigot, A proof calculus which reduces syntactic bureaucracy, Proceedings of the 21st International Conference on Rewriting Techniques and Applications of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.135-150, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00529301

J. Harrison, Handbook of Practical Logic and Automated Reasoning, 2009.
DOI : 10.1017/CBO9780511576430

J. Reed, Higher-order constraint simplification in dependent type theory, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice, LFMTP '09, pp.49-56, 2009.
DOI : 10.1145/1577824.1577832

G. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence, vol.4, pp.135-150, 1969.

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

L. Straßburger, Linear Logic and Noncommutativity in the Calculus of Structures, 2003.

L. Straßburger, Some Observations on the Proof Theory of Second Order Propositional Multiplicative??Linear??Logic, Typed Lambda Calculi and Applications, TLCA'09, pp.309-324, 2009.
DOI : 10.1007/BF01622878

A. Tiu, A Logical Framework for Reasoning about Logical Specifications, 2004.