VeTSS Summer School 2025 Programme

Monday 11th August Tuesday 12th August Wednesday 13th August Thursday 14th August
08:30 – 09:00 Breakfast at ARC Breakfast at ARC Breakfast at ARC
09:00 – 10:30 Arrival in Glasgow and check-in at the accommodation The Lean Programming Language and Theorem Prover Introduction to Program Synthesis Talk – Session 1
10:30  – 11:00 Morning break Morning break Morning break
11:00  – 12:30 The Lean Programming Language and Theorem Prover Introduction to Program Synthesis Talk – Session 2
12:30 – 14:00 Lunch Lunch Lunch / end of the school
14:00  – 15:30 Talk: Algebraic Effects Talk Travel back
15:30 – 16:00 Afternoon break Afternoon break Afternoon break
16:00  – 17:30 Lightning Talks Algebraic Effects Talk
17:30 – 18:00 End of day End of day End of day
18:00 Welcome Pizza dinner Social event Social event

The Lean Programming Language and Theorem Prover

Tuesday 12th August, Morning Session

Dr Sebastian Ullrich (LEAN Focused Research Organization, Germany)

BACKGROUND:

Lean is a functional programming language that can be also used as an interactive theorem prover. Lean programming primarily involves defining types and functions. This allows your focus to remain on the problem domain and manipulating its data, rather than the details of programming. The Lean project was launched by Leonardo de Moura in 2013 as an open source project, hosted on GitHub.

PREPARATION:

Additional materials may be circulated nearer the day, but students are asked to install Lean 4 on their machines in advance.

For installing Lean 4, please see their download pages. Information about the community of Lean users and the mathematical components library Mathlib can be found at the Lean Community website.

xxx

Wednesday 13th August, Afternoon Session

Dr Gethin Norman (University of Glasgow, UK)

BACKGROUND:

PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others. PRISM is based on rigorous, mathematical foundations and is particularly well suited to safety-critical applications, from assessing the reliability of airbag control software to building robust controllers for autonomous mobile robots in hazardous environments.

PRISM has been in continuous development for over 20 years and is the most widely used tool of its kind. Over 850 research papers have been published describing the tool, its applications and projects that build upon it. It has also been used in industrial projects and labs, from cloud computing at Fujitsu to fault-tolerant architectures at Honeywell and airbag safety at TRW Automotive. PRISM is open source software and has been adapted and enhanced by researchers worldwide. Its modelling language has become a de facto standard for representing probabilistic models within the formal verification community, and has been adopted and extended by many other tools.

PREPARATION:

Additional materials may be circulated nearer the day, but students are asked to install the latest version of PRISM on their machines in advance.