About the project
Formal methods have the potential to highly improve the quality of developed software, especially where programming errors can lead to costly faults. Promising examples exist that have formally shown the correctness of software for aviation control systems. However, formal methods are not widely used in industry. The main reason for this is that it is not taught to students prior to entering university. Students possess little to no prior knowledge or experience to relate to when presented with formal logic, types, semantics, or proof theory. However, computer science students are exposed to several courses on programming, so teaching logic and formal methods from a programmer's perspective is a useful way of aligning the course with their existing knowledge and skills, which can help them better understand and appreciate the value of these methods, ultimately leading to improved software quality and fewer costly faults.
Tools such as advanced text editors, interpreters, and similar programming language technologies are helpful aids when learning a new programming language. They persistently provide precise feedback to the programmer and thus remove some of the complexity of programming. Similarly, students can benefit from using such tools when learning proof theory in logic and semantics. The goal of this project will be to develop software (teaching tools), through which students can study the fundamental principles of reasoning by manipulating proofs as programs.
Background
The programming technology group in the Department of Informatics at the University of Oslo (UiO), is currently developing a course on advanced programming, semantics, and types. In this course, students will gain a deeper understanding of the theoretical aspects of programming by implementing fundamental concepts of programming languages, such as an interpreter and a type inferencer.
The research group “Theory of Programming Languages” at the Department of Computers and Informatics, Faculty of Electrical Engineering and Informatics, Technical University of Košice (TUKE), already teaches related classes on the subjects: Logic for informaticians, Type theory, and Semantics of Programming Languages.
Partners at both TUKE and UiO are interested in teaching and make such theoretical topics more interactive and relatable for students. In this bilateral project, TUKE and UiO will share their experiences in teaching logic, types, and semantics. We will collaborate in the development of new course materials for both parties (the new course at UiO, and existing course of logic at TUKE). We shall develop an interactive teaching tool and implement our results into the teaching process.
