The GRACE Spring School brings together doctoral candidates and invited researchers for a week of lectures, tutorials, and informal discussions on the themes at the heart of GRACE: Geometry, Representations and Algebra through Computation and Experiments. The school is part of the activities of the GRACE Doctoral Training Unit at the University of Luxembourg, funded by the FNR.

The programme combines short research talks given by GRACE doctoral candidates with longer lectures by invited speakers, a hands-on tutorial on interactive theorem proving in Lean, and a half-day excursion. It takes place in the small town of Clervaux, in the north of Luxembourg, whose castle and surrounding forests provide a quiet setting away from the everyday.

Location

Clervaux is a town in the Luxembourg Ardennes, nestled in a wooded valley around a twelfth-century castle and a striking neo-Romanesque parish church. It is reachable by direct train from Luxembourg City in about one hour.

View over Clervaux, with the church and the castle visible among the surrounding hills covered in autumn forest.
Clervaux, with its church (left) and castle (right), seen from the valley side.

Program

Talks given by doctoral candidates are 25 minutes long; lectures by invited speakers consist of two 30-minute sessions. The Lean tutorial (sessions Lean 1 to Lean 8) is given by Florent Schaffhauser. Titles and abstracts of all talks are available on the Abstracts page.

Sun 31 May Mon 1 Jun Tue 2 Jun Wed 3 Jun Thu 4 Jun Fri 5 Jun
08:00–09:00 — Breakfast Breakfast Breakfast Breakfast Breakfast
09:00–09:30 — Discussions Belmans Discussions Despré Discussions
09:30–10:00 — Welcome, GRACE Belmans Discussions Despré Discussions
10:00–10:30 — Veneziale Fisch Gehrunger Lean 5 Lean 7
10:30–11:00 — Veneziale Tognetti Gehrunger Lean 5 Lean 7
11:00–11:30 — Break Break Break Break Break
11:30–12:00 — Benoist Lean 1 Lean 3 Lean 6 Lean 8
12:00–12:30 — Boeren Lean 1 Lean 3 Lean 6 Lean 8
12:30–15:00 — Lunch, discussion Lunch, discussion Lunch, discussion Lunch, discussion Lunch, discussion
15:15–15:45 — Mahmoudian Lean 2 Lean 4 Excursion —
15:45–16:15 — Lidgren Lean 2 Lean 4 Excursion —
16:15–16:30 — Break Break Break Excursion —
16:30–17:00 — Fernández Píriz Page Usula Excursion —
17:00–17:30 — Hobohm Page Usula Excursion —
17:30–19:00 Discussions Discussions Discussions Discussions Discussions —
19:00–20:30 Dinner Dinner Dinner Dinner Dinner —
GRACE session Lean tutorial Excursion Meals & breaks
Titles and abstracts of the talks are listed on the Abstracts page.