So summing up the goals and scope of this course. The functional programming and the semantic communities have been and probably we feel, that is why we are here, we feel they will continue to be so. They have been the incubators of many concepts and tools which can support the development of dependable software in many ways. And the goal of this course is to illustrate some of these concepts and tools, especially the functional language ML and the proof assistant COQ. Together with the reasons for this success, which is the rigorous mathematical foundations. So, the course is intended for post-graduate students, young researchers in theoretical computer sciences and mathematics as well as software engineers who want to familiarise themselves with the foundations of some and probably many future formal methods in computer sciences

---