We study the foundations of the imperative and functional languages, including semantics and type systems. The special feature of this course is that theory is done in a very practical and hands-on way: we not just prove, but program all the results from first-principles. The basic tool used in the course is Coq proof assistant, which can be regarded as a functional programming language in its own right. It has been used, for example, to verify correctness of Java Card technology, C compilers or, more recently, fragments of x86 architecture.
Lernziele und Kompetenzen:
- The students explain the basics of both programming semantics and proof assistants, in particular Coq.
- The students prove theorems using a proof assistant.
- The students transfer proofs into programs and programs into proofs.
- The students examine behaviour of simple programs using formal semantics
- Evaluieren (Beurteilen)
- The students evaluate the role played by logic and type theory in scientific approach to programming.
- The students provide formal semantics to a simple programming language.