Per Martin-Löf og H-indekset

Per Martin-Löf (https://commons.wikimedia.org/wiki/File:Per_MartinLoef.jpg)

I vore dage er der gjort masser af forsøg på at kvantificere forskningspublikationers impact og på at måle styrken af forskningsresultater. Et mål er det såkaldte h-index. Et h-index på h, betyder, at man har h publikationer, der hver er citeret mindst h gange. Derfor kan man ikke have noget højt h-indeks, hvis man kun har få publikationer, selv om de så er citeret mange gange. Jeg har selvfølgelig også et h-indeks, og det er ikke så imponerende igen.

En af de mest indflydelsesrige personer i programmeringssprogenes nyere historie er formodentlig den svenske logiker Per Martin-Löf. Hans arbejde inden for intuitionistisk typeteori og specielt arbejdet med afhængige typer er centralt for programmeringssprog og bevisassistenter som Coq, Agda, Idris m.fl. Martin-Löf udviklede og implementerede ikke selv noget af dette, men hans indflydelse har været enorm. Hele arbejdet med formalisering af matematik og alle de praktiske resultater med maskintjekkede beviser af firefarvesætningen fra grafteori, Feit og Thompsons sætning fra gruppeteori m.m.m. ville være utænkeligt uden.

Der er et websted med alle Martin-Löfs artikler, og lidt afhængigt af hvordan man tæller, er der op til 33 publikation i perioden fra 1966 til 2014. Jeg ved ikke, hvad Martin-Löfs h-indeks er, men det kan ikke være så højt igen. Det er i sig selv tankevækkende.