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, 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, 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.

J. Brotherston, Cyclic Proofs for First-Order Logic with Inductive Definitions, Automated Reasoning with Analytic Tableaux and Related Methods: Proceedings of TABLEAUX 2005, pp.78-92, 2005.
DOI : 10.1007/11554554_8

R. Cleaveland, Tableau-based model checking in the propositional mu-calculus, Acta Informatica, vol.27, issue.8, pp.725-747, 1990.
DOI : 10.1007/BF00264284

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

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

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

A. Momigliano and A. Tiu, Induction and Co-induction in Sequent Calculus, Post-proceedings of TYPES 2003, number 3085 in LNCS, pp.293-308, 2003.
DOI : 10.1007/978-3-540-24849-1_19

L. Santocanale, A calculus of circular proofs and its categorical semantics, Proceedings of Foundations of Software Science and Computation Structures (FOSSACS02), number 2303 in LNCS, pp.357-371, 2002.
URL : https://hal.archives-ouvertes.fr/hal-01261170

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

C. Spenger and M. Dams, On the structure of inductive reasoning: Circular and tree-shaped proofs in the µ-calculus, FOSSACS'03, pp.425-440, 2003.

A. Tiu, Model Checking for ??-Calculus Using Proof Search, LNCS, vol.3653, pp.36-50, 2005.
DOI : 10.1007/11539452_7

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.