next up previous contents
Next: Bevisteoretiske Beregninger Up: Teoretisk Datalogi Previous: Processer

Typeteori

Typeteori er oprindelig udsprunget fra ønsket om at beskrive de langt rigere universer af data man finder i programmer end man finder f.eks. i fysikken. Typeteori opstod således udfra ønsket om at hjælpe programmørerne med at konstruere fejlfri programmer ved først at typebestemme alle data, beregninger og processer -- før programmøren beskrev beregningernes algoritmiske, eller processernes opførselsmæssige forløb. Men typeteori er gået langt videre. Som man kan løse mange opgaver i fysik ved almindelige dimensionsbetragtninger, således kan for eksempel udtryk i intuitionistisk typeteori beskrive beregninger. Man må nok idag konstatere at datalogisk typeteori er en af den teoretiske datalogi's fundamentalt nye bidrag til videnskaben -- og til matematikken?



Dines Bjorner
Fri Sep 5 08:26:58 MET DST 1997