  Theorem provers are tools that help users to write machine readable proofs.
Some of this tools are also interactive. The need of such softwares is
increasing since they provide proofs that are more certified than the hand
written ones. Agda is based on type theory and on the propositions-as-types
correspondence and has a Haskell-like syntax. This means that a proof of a
statement is turned into a function. Inference systems are a way of defining
inductive and coinductive predicates and induction and coinduction principles
are provided to help proving their correctness with respect to a given
specification in terms of soundness and completeness. Generalized inference
systems deal with predicates whose inductive and coinductive interpretations do
not provide the expected set of judgments. In this case inference systems are
enriched by corules that are rules that can be applied at infinite depth in a
proof tree. Induction and coinduction principles cannot be used in case of
generalized inference systems and the bounded coinduction one has been
proposed. We first present how Agda supports inductive and coinductive types
highlighting the fact that data structures and predicates are defined using the
same constructs. Then we move to the main topic of this thesis, which is
investigating how generalized inference systems can be implemented and how
their correctness can be proved.
