Content

Firstly, a general introduction will be given on the use of formal systems, their applications and on the typical structure and composition of a formal system. Afterwards, a number of concrete systems will be looked at in more detail. Which systems will be dealt with precisely will depend on each year. Possible systems include:
·         The lambda calculus and its application in the semantics of sequential programming languages;
·         The pi calculus and its application to the verification of protocols;
·         The spi calculus and its application to the specification and verification of the safety and security of distributed 
·         The ambient calculus and its application to the specification and verification of the safety of mobile code 
·         Formal type systems and their application in programming languages
·         Logics with module systems and graphical logics and their application to the specification of large systems

Course material

Study cost: Not applicable (The information about the study costs as stated here gives an indication and only represents the costs for purchasing new materials. There might be some electronic or second-hand copies available as well. You can use LIMO to check whether the textbook is available in the library. Any potential printing costs and optional course material are not included in this price.)

Content

First, a general introduction will be given on the use of formal systems, their applications and on the typical structure and composition of a formal system. Afterwards, a number of concrete systems will be looked at in more detail. Which systems will be dealt with precisely will depend on each year. Possible systems include:
·         The lambda calculus and its application in the semantics of sequential programming languages;
·         The pi calculus and its application to the verification of protocols;
·         The spi calculus and its application to the specification and verification of the safety and security of distributed 
·         The ambient calculus and its application to the specification and verification of the safety of mobile code 
·         Formal type systems and their application in programming languages
·         Logics with module systems and graphical logics and their application to the specification of large systems

*

Practical exercises with the lecture Formal Systems and their Applications. This can include the application of one of the formal systems studied to example problems, the design of a variant of an existing formal system, or the implementation of one of the formal systems studied in the course in order to perform some experiments.