Effectparametriciteit in afhankelijk getypeerde talen

Projectdetails

!!Description

Een functie in een imperatieve programmeertaal (bv. Java) kan neveneffecten veroorzaken zoals het tonen van output op het scherm of het gooien van een exception. Anderzijds kan een functie in een zuiver functionele taal (bv. Haskell) geen neveneffecten uitvoeren tenzij dit expliciet in het uitvoertype vermeld wordt. Zo zal een functie die een integer als argument neemt en een integer als resultaat teruggeeft of een exception gooit, als type int -> Excep(int) hebben. Hierbij is Excep(int) het type van berekeningen die een integer als resultaat hebben maar ook een exception kunnen gooien. Net zoals integers kunnen deze berekeningen gebruikt worden als argumenten van een andere functie of verzameld worden in een lijst. We kunnen bovendien andere types (bv. File(int)) contrueren om andere soorten van effecten weer te geven (bv. het uitlezen van een bestand). Effectpolymorfe functies zijn functies die kunnen werken met eender welke berekening, onafhankelijk van het soort effect dat die berekening kan veroorzaken. Effectparametriciteit is een mechanisme om te redeneren over effectpolymorfe functies. Afhankelijk getypeerde programmeertalen hebben een zeer sterk typesysteem zodat een programmeur tegelijk een programma kan schrijven en eigenschappen over dit programma in dezelfde taal kan bewijzen. In dit project passen we recent ontwikkelde ondersteuning voor parametriciteit in deze talen toe om effectparametriciteit te bestuderen.
AcroniemFWOTM978
StatusActief
Effectieve start/einddatum1/11/1931/10/21

Keywords

  • Programming languages
  • formal verification
  • side-effects

Flemish discipline codes

  • Language design, constructs and features
  • Language processors
  • Programming languages and technologies