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.

Finalmente: Roma!

navneskilt

Bortset fra endnu en Lufthansa-forsinkelse, der skyldtes en passager, der havde tjekket sin bagage ind men aldrig var dukket op selv (hvorfor den pågældende persons bagage skulle lokaliseres og fjernes fra flyet), gik resten af turen som den skulle. Dvs. det var underligt at sidde i flyet og vide at de andre var i gang med 1st Workshop on Behavioural Types (BEAT’13). Vi nåede frem til Hotel Parco dei Principi kl. 12.30 i dag, og de fleste deltagerne fra BEAT stod i foyeren og ventede. Vejret her er meget mildere end i Danmark; ikke antydningen af sne og temperaturer, der i Danmark ville passe bedre til april. Det var rart at kunne lægge vinterstøvler og vamset trøje i en pose for en stund.

Vi tog os en god og overraskende billig frokost på en café ved navn Gaudi. Italiernene sagde, at det ikke var en “rigtig restaurant”, men der var venlig betjening og hyggeligt interiør. I brødkurven var der noget, der lignede æbleskiver ; det var pizzadej dybstegt i olivenolie. En simpel og forbløffende delikat oplevelse, men nok ikke god, hvis man vil tabe sig. Der var en stor frokostbuffet, og jeg lærte udtrykket kilometro zero, der vist nærmest kan oversættes til “årstidens lokale grøntsager” (som man skal 0 kilometer væk for at hente – vel lidt af en overdrivelse, i al fald når man taler om centrum af Rom).

Mange af os er også med i det nye forskernetværk BETTY (det, der tilbage i oktober fik sendt mig til opstartsmøde i Bruxelles) og her fik vi snakket om hvordan vi skal lave det rigtige opstartsmøde til marts. Det bliver forresten også her i Rom.

Jeg fik desværre kun hørt de tre sidste foredrag til BEAT og gik bl.a. glip af Naoki Kobayashis gennemgang af hans resultater om adfærdstyper; Naoki har engang besøgt mig i Aalborg og han holder nogle rigtig gode og klare foredrag.

Thomas Hildebrandts foredrag havde jeg allerede hørt ugen inden i Aalborg. Vasco Vasconcelos fortalte først om Kohei Honda, der døde så pludseligt i sidste måned, og derefter om sit eget nye arbejde, der lader lineære typer og korrespondanceudsagn møde sessionstyper. Og til sidst gav Jakob Rehof (der er dansker, men snart i mange år har været i Dortmund, hvor han er professor og leder af Fraunhofer-instituttet) et spændende foredrag, hvor gamle resultater fra matematisk logik, nærmere bestemt Tarskis gamle arbejde med bevisbarhed i udsagnslogik og Church, Schönfinkel m.fl.’s arbejde med typet kombinatorlogik, kan bruges til at forklare, hvordan man ud fra et programbibliotek (hvor programmerne er typede kombinatorer) kan syntetisere et nyt program. Det hele er selvfølgelig muligt pga. Curry-Howard-isomorfien mellem typer og udsagn og det hele er selvfølgelig også enten uafgørbart eller (i specialtilfælde) EXPTIME-fuldstændigt, sådan som mange spændende beslutningsproblemer desværre skal være.

Og den egentlig ret lange dag endte på en ristorante, hvor Juventus spillede 1-1 mod Lazio i baggrunden og de italienske deltagere i selskabet kappedes om at fordømme Silvio Berlusconi.