Meetings

4th meeting - 22.04.2024 - 26.04.2024

Team members from the Technical University of Košice (Perháč, Steingartner, Chodarev, Novotný) visited the University of Oslo.

3rd meeting - 26.02.2024 - 01.03.2024

Team members from the University of Oslo (Joachim Tilsted Kristensen, Lars Vadgaard, and Michael Kirkedal Thomsen) visited the Technical University of Košice.

The team members met at the Technical University in Košice

We have started to implement the teaching tool, that we call the OnlineProver. During the meeting, we have been implementing the two backend programming languages, for specifying a language and a set of exercises. We have also formulated example programs in both programming languages, and started to write a manual and a test suite for the project. Exercises can now be sent to the frontend, rendered, filled out, and sent back to the server. The final parts of the proof checking remain to be implemented. Regarding the frontend: We have implemented the core functionality (a visual natural deduction tree editor) for the OnlineProver before the meeting. We have designed the protocol between the frontend and backend and have the frontend respect that protocol and render the exercises received from the backend.

Regarding publicity:

We have continued to work on a survey paper on the use of theorem provers in teaching computer science students. We have finished the first selection stage by creating queries for the most popular STEM scientific databases: Web of Science, Scopus, ACM DL, and IEEE Xplore based on the PICOC keywords.
We prepared the extended abstract for the TYPES’24 conference.
We have started the paper at the ITP’24 conference. This led to discussions on the teaching approach and evaluation of the use of OnlineProver in teaching.
Additionally, the team members from UiO have given two guest lectures:
- Michael Kirkedal Thomsen: Program Transformation, Partial Evaluation and the Futamura Projections (Formal languages).
- Joachim Tilsted Kristensen: Introduction to Logic Programming in Prolog (Logic for informaticians).

2nd meeting - 13.11.2023 - 17.10.2023

Team members from the University of Oslo (Eric Bartley Jul, Joachim Tilsted Kristensen, Lars Vadgaard, and Michael Kirkedal Thomsen) visited the Technical University of Košice.

The team members met at the Technical University in Košice

We have addressed the initially proposed outcomes of the initiative. They are

Lecture notes for the course “Programming Language Implementation and Formalisation” (UiO).
Lecture notes for the course “Logic for informaticians” (TUKE).
A digital tool onlineprover.com to use for providing and solving exercises in natural deduction (Gentzen style).
A survey paper that analyzes the state-of-the-art for such tools.
A user interface for interacting with the tool in a browser.
A collection of teaching scenarios that we want to try out in future work.

There was a discussion about approaches to teaching relevant subjects, which gave rise to ideas on how to improve the teaching process on both sides. The possibilities of how to implement the proposed improvements into the teaching process were discussed. The software requirements of the proposed teaching tool were developed.

We have developed informal semantics for a second iteration of the prototype DSL language, which is going to be more like a Lex/Yacc implementation with a special notion of pattern matching. We have also discussed the user interface, and came up with a new design.

Additionally, the team members from UiO have given three guest lectures in master courses.

Michael Kirkedal Thomsen : Reversible quantum computing (Semantics of programming languages).
Joachim Tilsted Kristensen: Continuation passing style (Functional programming).
Joachim Tilsted Kristensen: Proofs as programs (Type theory).

Photos

1st meeting - 14.10.2023 - 20.10.2023

Team members from the Technical University of Košice (Perháč, Steingartner, Chodarev, Novotný) visited the University of Oslo.

Team members met at the University of Oslo and started to work on the solution to the proposed initiative results. We have engaged in discussions about each other’s approaches to teaching relevant courses, proposed ideas on how to improve the teaching process on both sides, and possibilities of how to implement proposed improvements into it. We have also discussed the proposed teaching tool’s requirements and created the software requirements that shall be implemented.

Achievements: