POPL

popl
Udsigt over parallelfrokost nr. 1 ved POPL 2013.

I dag startede hovedkonferencen Principles of Programming Languages, bedre kendt som POPL. POPL er på mere end én måde en af de største konferencer, jeg har været til (jeg har været med flere gange tidligere). For det første er antallet af deltagere overvældende stort – der er så mange, at der er tre parallelle frokost-serveringer i tre store lokaler. Dét har jeg aldrig set før, heller ikke til de tidligere POPL, jeg har deltaget i. Og for det andet er kvaliteten af bidragene rigtig høj. Det er måske ikke alt, der er lige spændende for alle og heller ikke for mig, men jeg bed mig som sædvanlig fat i nogle foredrag.

Dagens første foredrag var et indbudt foredrag af Georges Gonthier fra INRIA/Microsoft Research, der fortalte om det maskintjekkede bevis for Feit-Thompsons sætning om entydig faktorisering af grupper af ulige orden. Det har jeg tidligere skrevet om her. Gonthier fortalte først om sætningen og dens gruppeteoretiske grundlag og dernæst om arbejdet med at repræsentere beviset i typeteorien Calculus of Constructions eller rettere i værktøjet Coq, der er en implementation af denne. Den helt centrale indsigt som Feit og Thompson gjorde var at betingelserne for at være en gruppe, der ikke opfylder entydighedsbetingelsen i sætningen kan fanges i Galois-teori. Men det betyder så også at en repræsentation i Coq skal fange en hel masse standardbegreber i gruppeteori og resultater om dem – helt fra simple begreber som grupper, normale undergrupper og sideklasser over Sylows sætninger, Frobenius-grupper og sætninger i Galois-teori. Intet under at det tog så mange mennesker så lang tid at lave dette maskintjekkede bevis; én ting er at forstå gruppeteorien, en anden er at beskrive den inden for typeteori og formalisere hvert eneste lille lemma i Coq. Gonthiers foredrag var lidt for langt og af og til fortabte han sig i de mange interessante detaljer af både matematisk, typeteoretisk og mere programmeringsnær art, dette imponerende projekt rummer. Men jeg hæftede mig ved to ting. For det første lader det til at “rigtige” algebraikere (ifølge Gonthier) synes at dette er spændende. For det andet opdagede Gonthier og hans kolleger undervejs at der faktisk var en træls trykfejl i Feit og Thompsons artikel, der sneg sig videre fra den første af deres første lange artikler med det oprindelige bevis ind i den anden – men at denne trykfejl ingen betydning havde, da den optrådte i en betingelse, der i det computertjekkede bevis viste sig at være overflødig!

Der var også andre interessante foredrag om bl.a nominelle mængder (et emne, jeg selv er endt med at berøre), om typeinferens for forfiningstyper (et andet emne, jeg engang kastede mig over – men min tidligere samarbejdspartner Naoki Kobayashi opdagede at han kunne genbruge et trick med at reducere dette problem til løsning af lineære uligheder!) og et spændende foredrag af Sam Staton om hvordan man kan forstå typereglerne for funktionsorienterede programmeringssprog ved brug af kategoriteori. Alle tre foredrag rummede resultater af stor værdi, men hvad bedre var: foredragsholderne fik præsenteret de vigtige ideer uden at fortabe sig i detaljer. Det er bestemt ikke altid at selv et foredrag på en prestigefyldt konference når ud over scenekanten.

Jeg blev væk fra nogle foredrag for at tage en lille tur ud i byen. Jeg fik skimtet Colosseum og Vittorio Emmanuele-monumentet i det fjerne og det gik op for mig, at jeg var havnet i samme del af den italienske hovedstad som jeg havde set, sidst jeg var for over 26 år siden! En mindre stolt oplevelse er at jeg ikke kunne finde ud af at tage bussen – eller rettere: Det kunne jeg godt, men jeg vidste ikke, at man ikke kunne købe billetter i bussen. De kan købes i kiosker og tobaksforretninger og kun dér. Så hvis buschaufføren læser dette indlæg, kan han vel egentlig afkræve mig kontrolafgift for at have kørt i bus uden billet (jeg fik dog købt en billet på tilbagevejen).

Internetforbindelsen på mit hotel er ikke fantastisk, vel ofte sammenlignelig med gamle dages 28 kilobaud-modemmer, og til konferencen er forbindelsen hurtigere men til gengæld ekstremt overbelastet (vel at forvente, når man placerer flere hundrede mennesker med hver deres computer i samme lokale), så underligt nok er jeg mere offline end jeg ellers er på rejse. Til gengæld lærer jeg en del om stoisk tålmodighed på denne rejse af dårlige netforbindelser og køer i lufthavne og hoteller og til servering af mad og drikke; det er måske ikke så overraskende, at stoicismens vigtigste repræsentanter Seneca og Marcus Aurelius var romere.

(Visited 32 times, 1 visits today)
Loading Facebook Comments ...

Skriv et svar