The goal of this course is to introduce the idea of the formal, mathematical definition of programming languages, and their implementation in an interactive theorem prover, Coq. We will be discussing the motivation of this theory, and we will overview some fundamental approaches to defining precise program semantics, including operational and denotational techniques. Understanding of the main concepts will be deepened by defining simple languages both in mathematical terms and in the Coq theorem prover. After completing the course, participants will better understand how program execution is modelled and how one can carry out formal arguments about the correctness of program behaviour in Coq.
Course leader
ELTE- Faculty of Informatics
Target group
Participants are expected to have basic knowledge in set-theoretic foundations of mathematics, mathematical logic, the theory of formal languages, and functional programming.
Course aim
The goal of this course is to introduce the idea of the formal, mathematical definition of programming languages, and their implementation in an interactive theorem prover, Coq.
Credits info: 3 EC
Our courses offer ECTS points, which may be accepted for credit transfer by the participants' home universities. Those who wish to obtain these credits should inquire about the possible transfer at their home institution prior to their enrollment. The International Strategy Office will send a transcript to those who have fulfilled all the necessary course requirements and request one.
Fee info
EUR 470: The course fee - that includes tuition fee, accommodation (student residence halls with shared rooms 2-3/ room), meals (breakfast and lunch for each day), local transport and the cost of the leisure time programs - is 470 EUR
For further information, please click the "LINK TO ORIGINAL" button below.