The broad objective of this thesis is to give evidence to the fact that {\em Final
Semantics}, originated and developed  by Aczel and Rutten, is a quite general
methodology for semantics. We  show in fact that it can apply equally fruitfully to
{\em process algebra} languages, {\em higher order imperative concurrent}
languages, {\em functional} languages, and {\em calculi for mobile processes}.
But furthermore, we show that Final Semantics can be successfully carried out {\em
already} in naive set-theoretical categories, without having to resort to complex
mathematical settings. Hence this thesis can be viewed also as an investigation in
the applicability of {\em hypersets}. {\em Final Semantics} is a principled way of
understanding, and hence manipulating and  reasoning rigorously on, those infinite
and circular objects and those recursively defined notions, which arise in
computation theory through some kind of {\em maximal fixed point} definition. In
this thesis we carry out investigations of maximal fixed points from {\em
set-theoretical}, {\em categorical}, and {\em logical} standpoints. In particular,
we discuss the purely set-theoretical account of {\em coinduction principles} and
{\em coiterative functions}. We give a  categorical generalization of this account
in terms of {\em final coalgebras},  which encompasses a great deal of the
diversity of coinduction schemes. We discuss also logical axiomatizations of
largest bisimulation equivalences on syntactical objects. We develop both
syntactical and semantical techniques for giving coinductive descriptions of
observational (contextual) equivalences, thereby  providing a number of (often new)
coinduction principles for reasoning on program and process behaviour.