< Terug naar vorige pagina

Project

Ontwikkeling van technieken voor het opleggen van regels voor information flow.

Alle software wordt voorgesteld als broncode in een programmeertaal. De programmeertaal bepaalt de betekenis of semantiek van de code, bijvoorbeeld haar operationeel gedrag. Uitvoerbare broncode wordt vaak vergezeld door bijkomende specificaties die definiëren hoe de broncode moet geïnterpreteerd worden of extra informatie geven over de semantiek van de software. Ze maken het mogelijk voor programmeurs om uit te drukken en te verifiëren dat hun software de bedoelde semantiek heeft en om semantische veronderstellingen uit te drukken tussen componenten onderling. Goede representaties en specificaties van softwarecomponenten zijn cruciaal om efficiënt software te produceren die betrouwbaar, performant en veilig is en om deze kwaliteiten te blijven garanderen tijdens de evolutie van de software. Veel soorten softwarecomponenten en hun gewenste semantische eigenschappen zijn moeilijk voor te stellen of te specifiëren. In deze thesis draag ik nieuwe functionele technieken bij voor de voorstelling en specificatie van vier soorten softwarecomponenten:
  • ad hoc-polymorfe functies: functies wiens gedrag afhangt van het type van hun argumenten of resultaat. Ik stel instance arguments voor: een typesysteemuitbreiding voor het voorstellen van ad hoc-polymorfe functies in de afhankelijk-getypeerde (dependently-typed) programmeertaal Agda. In vergelijking met bestaande voorstellen, introduceren instance arguments geen bijkomend structureel concept en zijn functies die instance arguments gebruiken volwaardig ondersteund. Daarenboven vermijden ze de toevoeging van een afzonderlijke en krachtige vorm van uitvoering op type-niveau. Bestaande Agda libraries die records gebruiken hoeven ook niet te worden aangepast om ze te gebruiken. Mijn implementatie is een deel van Agda sinds versie 2.3.0 en ik toon verschillende toepassingen van instance arguments.
  • Contextloze grammaticas: een standaardtechniek voor het definiëren van formele talen. Ik stel een techniek voor om contextloze grammaticas voor te stellen in een ingebedde domein-specifieke programmeertaal (EDSL). De techniek vermijdt de beperkingen van bestaande parser-combinatorbibliotheken met behulp van een vernieuwende expliciete voorstelling van recursie, gebaseerd op geavanceerde typesysteemtechnieken in de Haskell programmeertaal. Als bijkomend voordeel worden grammaticas losgekoppeld van semantische acties. Aan de andere kant vereist de aanpak dat de grammatica-auteur een codering voorziet van het domein van de grammatica op type- en waardeniveau, en kan ik slechts een beperkte versie voorzien van constructies als many. Ik demonstreer de aanpak met vijf grammatica-algoritmes, o.a. een weergeefalgoritme (pretty-printer), een bereikbaarheidsanalyse, een vertaling van gekwantificeerde recursieconstructies naar gewone en een implementatie van de linkerhoek- of left corner-grammaticatransformatie. Dit werk vormt de basis van mijn grammar-combinators parsing-bibliotheek.
  • Meta-programmas: programmas die andere programmas genereren of manipuleren. Ik stel vernieuwende meta-programmeerprimitieven voor voor gebruik in een afhankelijk-getypeerde functionele programmeertaal. De types van de meta-programmas leveren sterke en precieze garanties over hun terminatie, correctheid en volledigheid. Het systeem ondersteunt type-veilige constructie en analyse van termen, types en typeringscontexten. In tegenstelling tot andere aanpakken, worden ze geschreven in dezelfde stijl als normale programmas en gebruiken ze het standaard functioneel uitvoeringsmodel van de programmeertaal. Ik formaliseer de nieuwe meta-programmeerprimitieven, implementeer ze als een uitbreiding van Agda en lever bewijs van hun nut met twee overtuigende toepassingen in de domeinen van datatype-generisch programmeren en bewijstactieken (proof tactics).
  • Effect-polymorfe software. Statische APIs met neveneffecten en globale wijzigbare toestandinformatie in object-georiënteerde programmeertalen maken het moeilijk om effecten modulair te controleren. Object-bekwaamheidsprogrammeertalen (Object-Capability of OC) lossen dit probleem op door af te dwingen dat effecten alleen kunnen veroorzaakt worden door componenten die een referentie hebben naar het object dat de bekwaamheid voorstelt om dat te doen. Ik bestudeer deze inkapseling van effecten door een formele vertaling naar een getypeerde functionele calculus met hogere-rang polymorfisme (ik gebruik een beperkte versie van Haskell voor de presentatie). Op basis van een informele visie van effect-polymorfisme als het fundamentele kenmerk van OC-talen,vertaal ik een OC calculus naar effect-polymorfe Haskell code, d.w.z. berekeningen die uniform gekwantificeerd zijn over de monade waarin ze effecten veroorzaken. De types van onze vertalingen drukken de object-bekwaamheidseigenschap uit en we kunnen dit aantonen en gebruiken met behulp van Reynolds parametriciteitsstelling. Een belangrijk nieuw inzicht is dat bestaande OC talen en formalisaties één effect impliciet beschikbaar laten: de allocatie van nieuwe wijzigbare toestandsinformatie; hier een bekwaamheid voor toevoegen heeft belangrijke theoretische en praktische voordelen. Mijn werk opent een belangrijke nieuwe verbinding tussen object-bekwaamheidsprogrammeertalen en de goed onderzochte velden van functioneel programmeren en denotationele semantieken.
Datum:22 jun 2009 →  30 sep 2014
Trefwoorden:Information flow control, Security, Software, Computer science
Disciplines:Toegepaste wiskunde, Computerarchitectuur en -netwerken, Distributed computing, Informatiewetenschappen, Informatiesystemen, Programmeertalen, Scientific computing, Theoretische informatica, Visual computing, Andere informatie- en computerwetenschappen
Project type:PhD project