On the expressivity of typed concurrent calculi

De expressiviteit van getypeerde programmeertalen

Deze scriptie begint aan een uitgebreide verkenning van formele computationele modellen die ten grondslag liggen aan getypeerde programmeertalen. De focus ligt op programmeercalculi, zowel functioneel (sequentieel) als concurrent, omdat zij een overtuigend rigoureus kader bieden voor het evalueren van programmasemantiek en voor het ontwikkelen van analyses en programmaverificatie.

Concreter richt Joe Paulus zich op de volgende onderzoeksvraag: hoe generaliseert interactief gedrag precies sequentiële berekening? Hij probeert de expressiviteit van de π-calculus---de paradigmatische calculus van gelijktijdigheid en interactie---te meten met betrekking tot de sequentiële berekening zoals vastgelegd door de λ-calculus. Voortbouwend op Milner's baanbrekende werk over 'functies als processen', contrasteert deze benadering deze twee fundamentele computationele modellen via correcte vertalingen, die formeel uitleggen hoe sequentiële termen in λ kunnen worden gecodificeerd in gelijktijdige processen in π. Paulus' belangrijkste bijdrage is het gebruik van gedragstypes, geavanceerde typesystemen voor termen (in λ) en processen (in π), om de calculi te definiëren, de eigenschappen van getypeerde termen/processen vast te stellen en om de correctheid van zijn vertalingen te bewijzen.

Paulus benaderde zijn onderzoeksvraag vanuit verschillende dimensies. Ten eerste beschouwde hij niet-deterministische berekeningen, waarbij reducties vertakkingsgedrag kunnen vertonen. Niet-determinisme brengt flexibiliteit en algemeenheid in specificaties; het kan confluent of niet-confluent zijn: in het eerste geval kunnen reducties onafhankelijk binnen alternatieve vertakkingen worden genomen, op een niet-committerende manier; in het laatste geval sluit het kiezen voor een vertakking andere alternatieven uit.Als een andere dimensie beschouwde hij ook resource-bewuste berekeningen waarbij bronnen lineair (exact één keer bruikbaar) of onbeperkt (nul of meerdere keren bruikbaar) zijn. Resource-bewustzijn maakt op zijn beurt de weg vrij voor een principiële, expliciete behandeling van fouten in berekeningen, die kunnen optreden wanneer er een tekort of overschot aan middelen is of wanneer ze verkeerd worden gebruikt.

Een belangrijk inzicht is dat intersectietypes in de λ-calculus kwantitatieve informatie van een term nauwkeurig kunnen specificeren naarmate deze door de berekening evolueert. Door strakke, type-behoudende vertalingen te bieden tussen intersectietypes (in λ) en sessietypes (in π) legt Paulus een originele verbinding tussen deze twee belangrijke en veel bestudeerde typedisciplines langs de genoemde dimensies.Ten slotte contrasteerde Paulus modellen van sequentiële en gelijktijdige berekening door typesystemen voor gelijktijdigheid te beschouwen die terminatie garanderen (sterke normalisatie): dit is een goed bestudeerde en fundamentele eigenschap voor sequentiële berekeningsmodellen, die actief wordt bestudeerd in de gelijktijdige setting.

Joe Paulus voerde zijn promotieonderzoek uit aan het Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, afdeling Fundamentele Informatica. Hij vervolgt zijn loopbaan als Associate Researcher bij Oxford University. 

Proefschrift: https://hdl.handle.net/11370/41054198-864c-44d9-ab7c-8ac8c3c91137