Let me just mention a few formal systems that we will describe in this course… Well, we will briefly touch upon the l-calculus. We will put a lot of emphasis on the p-calculus, that is a calculus for describing processes and we will briefly touch upon the ambient-calculus, which has been recently introduced especially for addressing the problems arising in global computing and in mobile computing. So this is especially interesting for mobile computing.
Then we have to process algebras, different ways of dealing various semantics operational, denotational, logical.
We have various logics all stemming from Hoare's logic and going to model and temporal logic. We have all the family of constructive type theories.
There is something else that we do not want to do. We have this plethora of the formal systems. Well, we do not want to start over from first principle. The study of the meta-theory of each and everyone of these. When we want to build an interactive tool for dealing with these systems, we do not want to start from scratch each time. We want to be able to re-use the software that we have built for building an assistant for any of these systems for another such system.