De fleste programmører bruger allerede grundlæggende typesystemer i for eksempel C# eller Java, og måske har du også prøvet mere avancerede typesystemer i sprog som F#, Rust eller TypeScript. Disse typesystemer er dog forholdsvis primitive set fra et nutidigt forskningsperspektiv: Vi giver her et indblik i, hvor langt man kan gå med state-of-the-art værktøjer.

Arrangementet er en introduktion til de såkaldte bevisassistenter, som kan opfattes som funktionsprogrammeringssprog tilsat matematisk logik.

Vi viser, hvordan værktøjer som Coq og Isabelle gør det muligt at bevise korrektheden af compileroptimeringer, programmere styresystemer helt uden sikkerhedshuller og designe chips, der altid regner rigtigt. Samtidig gives også et indblik i, hvordan du selv kan benytte bevisassistenter i det daglige arbejde og et bud på, hvilke tendenser vi kommer til at se i den nærmeste fremtid.

Forudsætninger: Der er ingen særlige, men det er en fordel at kende lidt til funktionsprogrammering.

Foredragsholdere: Frederik Krogsdal Jacobsen og Jørgen Villadsen (DTU Compute).

Arrangør: Finn Gustafsson, IDA IT

Gratis for medlemmer af IDA IT og DANSK IT

Forplejning: Kaffe/te og frugt/sodavand.