Kansliets noteringar
Kod

Dnr

2013-2993-108682-9

Area of science

Natural and Engineering Sciences
Announced grants

Grants for distinguished young researchers 2013

2013
Grants for distinguished young
researchers

Total amount for which applied (kSEK)
2013

2014

2015

2016

2017

APPLICANT
Name(Last name, First name)

Date of birth

Gender

Jansson, Patrik

720311-7515

Male

Email address

Academic title

Position

patrikj@chalmers.se

Professor

Biträdande professor

Phone

Doctoral degree awarded (yyyy-mm-dd)

031-7725415

2000-06-19

ADMINISTRATING ORGANISATION
Administrating Organisation

Chalmers tekniska högskola

WORKING ADDRESS
University/corresponding, Department, Section/Unit, Address, etc.

Chalmers tekniska högskola
Institutionen för data-och informationsteknik
Programvaruteknik
41296 Göteborg, Sweden

PROPOSED HOST ORGANISATION
University/corresponding, Department, Section/Unit, Address, etc.

Chalmers tekniska högskola
Institutionen för data-och informationsteknik
Programvaruteknik
41296 Göteborg, Sweden

UNIVERSITY, FACULTY AND DEPARTMENT FOR DOCTORAL EXAM
Co-Operating University 1

Chalmers

DESCRIPTIVE DATA
Project title, Swedish (max 200 char)

Starkt typade bibliotek för program och bevis

Project title, English (max 200 char)

Strongly Typed Libraries for Programs and Proofs

Abstract (max 1500 char)

Our long-term goal is to create systems (theories, programming languages, libraries and tools) which make it easy to develop
reusable software components with matching specifications. In this research project, the main focus is on libraries. Strongly-typed
programming languages allow to express functional specifications as types. Checking the types of a program then means checking it
against its specification. Within such powerful programming languages, libraries are not

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

Kod

2013-2993-108682-9
Name of Applicant

Jansson, Patrik
Date of birth

720311-7515

only building blocks of programs, but also of proofs. We believe that such libraries will eventually become the main means of
developing programs, and because they come with strong types, the programs built using the library will come with strong properties
that will make the whole easy to prove correct. The production of such libraries will also inform the design of future strongly-typed
programming languages. In the recent years, strongly-typed programming languages have started to become usable, but remain
confined to a small niche. Our libraries will make them a viable solution for a broader range of applications, bringing higher
guarantees of correctness to a wider user base. To check the applicability of our libraries, we will apply them to classical problems of
computer programming, such as certain divide-and-conquer algorithms or optimisation problems, as well as to the construction of
tools supporting dependently-typed programming themselves.

Abstract language

English
Keywords

Software Technology, Functional Programming, Dependent Types, Program Verification, Generic Programming
Review panel

NT-FYF
Classification codes (SCB) in order of priority

10201, 10205, 10103
Aspects

ENCLOSED APPENDICES
A, B, C, S

APPLIED FUNDING: THIS APPLICATION
Funding period (planned start and end date)

2013-01-01 -- 2019-12-31
The amount is predetermined by the Swedish Research Council.
Popularscience heading and description (max 4500 char)

En viktig gren av forskningen inom datavetenskap handlar om att utveckla system (programspråk, verktyg, programbibliotek, teorier)
som gör det enkelt att konstruera programvara som är korrekt och återanvändbar. Detta projekt siktar på att utnyttja funktionella
programspråk med starka typsystem till att skapa bibliotek av komponenter som kan uttrycka både specifikationer och
implementationer som uppfyller dessa. Vi kommer att utnyttja datorstödd interaktiv programutveckling där automatiska verktyg ger
snabb återkoppling på vilka delar som inte uppfyller specifikationen.
Den teoretiska möjligheten att uttrycka program och bevis i samma programspråk är känd sedan många år, men det är först nyligen
som teknikutvecklingen har medgett att utveckla större programbibliotek på detta sätt. Detta innebär att det finns många spännande
grundläggande frågor kvar att utforska och vi avser börja med enkla algoritmer för att sedan steg för steg utforska hur långt det går
att komma. Vi arbetar iterativt i tre nivåer för att utveckla komponentbiblioteken. Första nivån är att implementera en lösning på ett
visst problem (sökning, optimering eller liknande), nästa nivå är att abstrahera ut gemensamma mönster till programbibliotek och
slutligen vill vi utvärdera vilka möjliga förändringar av den underliggande språket som skulle kunna förbättra resultaten. Inom projektet
kommer vi att arbeta fram korrekta generiska bibliotek uttryckta i språket Agda. Agda är ett verktyg baserat på typteori och funktionell
programmering

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

Kod

2013-2993-108682-9
Name of Applicant

Jansson, Patrik
Date of birth

720311-7515

som möjliggör utveckling av program och specifikationer i samma språk. Utvecklingen av språket har skett (och forskrider parallellt
med biblioteksprojektet) i ett internationellt samarbete (med Japan, Tyskland och England) lett av Chalmers.
På lång sikt kan bevisbart korrekta programbibliotek användas och återanvändas som byggstenar vid all slags
programvarukonstruktion. Detta ger allmänt sett mer pålitliga program, och färre buggar. Ett spännande applikationsområde är
exekverbara, överblickbara högnivåmodeller för komplexa system. Vi har hittills mest fokuserat på att modellera komplexa system
inom dataområdet (logiska ramverk, lingvistik, programspråk, hårdvara) men i samarbetet med Potsdams Institut för Klimatforskning
(PIK) har vi börjat arbeta med komplexa system i interaktionen mellan klimat, ekonomi och samhälle. PIK har under flera år arbetat
med simuleringar av komplexa system och har under senare år börjat använda funktionell programmering som ett verktyg för att
experimentera med och kommunicera de högnivåmodeller som behövs för att överblicka komplexa system. Dessa högnivåmodeller
översätts senare i flera steg till effektiv programkod som klarar att köra tunga simuleringar inom rimlig tid. (Dessa simuleringar ger
underlag till politiska beslut inom klimatområdet.) PIK tog kontakt med Chalmers för att fördjupa sin kompetens inom
högnivåmodellering med hjälp av moderna programspråk (som Haskell och C++) och vi har under åren som gått haft flera kontakter
där starkt typade bibliotek för program och bevis har utkristalliserats som det forskningsområde där Chalmers bäst kan komplettera
PIK. Samarbetet har lett till ett gemensamt EU-projekt, flera artiklar och bibliotek för program och bevis.
På Chalmers leds projektet av Patrik Jansson (inom gruppen Funktionell Programmering). Jansson har forskat om generisk
programmering sedan 1995 i olika konstellationer och det internationella kontaktnätet är mycket starkt. Den lokala forskningsmiljön
inom D&IT-institutionen är världsledande även inom flera närliggande områden - automatisk testning (Hughes, Claessen),
domänspecifika språk (Sheeran, Claessen), typteori (Coquand), språkteknologi (Ranta).

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

Kod

þÿ2013-2993-10Z6Z2-9
Name of applicant

Jansson, Patrik
Date of birth

720311-7515
Title of research programme

Strongly Typed Libraries for Programs and Proofs

Appendix

A

Research programme

VRAPS/VR-Direct bilaga 2004.Ae

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

❙tr♦♥❣❧② ❚②♣❡❞ ▲✐❜r❛r✐❡s ❢♦r Pr♦❣r❛♠s ❛♥❞ Pr♦♦❢s
✶ P✉r♣♦s❡ ❛♥❞ ❛✐♠s

t❡r♥✳

❖✉r ❧♦♥❣ t❡r♠ ❣♦❛❧ ✐s t♦ ❝r❡❛t❡ s②st❡♠s ✭t❤❡✲

r✐s❦ ♦❢ s♦❢t✇❛r❡ ❡rr♦r ❣r♦✇s ✇✐t❤ t❤❡ s✐③❡ ♦❢

♦r✐❡s✱ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥❣✉❛❣❡s✱ ❧✐❜r❛r✐❡s ❛♥❞

t❤❡ ♣r♦❣r❛♠✳

t♦♦❧s✮ ✇❤✐❝❤ ♠❛❦❡ ✐t ❡❛s② t♦ ❞❡✈❡❧♦♣ s♦❢t✇❛r❡

✐♥ t❤❡ ❡✈♦❧✉t✐♦♥ ♦❢ ♥❡✇ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥✲

❝♦♠♣♦♥❡♥ts ❛♥❞ ♠❛t❝❤✐♥❣ s♣❡❝✐✜❝❛t✐♦♥s✳ ■♥

❣✉❛❣❡s ✐s ✐♠♣r♦✈❡❞ s✉♣♣♦rt ❢♦r ❛❜str❛❝t✐♦♥✖

t❤✐s r❡s❡❛r❝❤ ♣r♦❥❡❝t✱ ✇❡ ❛✐♠ t♦ ❧❡✈❡r❛❣❡ t❤❡

♠❛❦✐♥❣ ♠♦r❡ ❛♥❞ ♠♦r❡ ♦❢ t❤❡ ❧❛♥❣✉❛❣❡ ❢❡❛✲

♣♦✇❡r ♦❢ ❧❛♥❣✉❛❣❡s ✇✐t❤ str♦♥❣ t②♣❡s t♦ ❝r❡✲

t✉r❡s ♣r♦❣r❛♠♠❛❜❧❡✳

❛t❡ ❧✐❜r❛r✐❡s ♦❢ ❝♦♠♣♦♥❡♥ts ✇❤✐❝❤ ❝❛♥ ❡①✲

❧❛♥❣✉❛❣❡s ❛r❡ ❛❝t✐✈❡❧② ❣❛✐♥✐♥❣ ❛❜str❛❝t✐♦♥

♣r❡ss ❢✉♥❝t✐♦♥❛❧ s♣❡❝✐✜❝❛t✐♦♥s ✐♥ ❛ ♥❛t✉r❛❧

♣♦✇❡r ✇✐t❤ ❏❛✈❛ ●❡♥❡r✐❝s✱ ❈✰✰ ❚❡♠♣❧❛t❡s✱

✇❛②✱ ❛♥❞✱ s✐♠✉❧t❛♥❡♦✉s❧②✱ ✐♠♣❧❡♠❡♥t❛t✐♦♥s

❙❝❤❡♠❡✬s ❝♦♠♣♦s❛❜❧❡ ♠❛❝r♦s ❛♥❞ ❍❛s❦❡❧❧

✇❤✐❝❤ s❛t✐s❢② t❤♦s❡ s♣❡❝✐✜❝❛t✐♦♥s✳ ❚❤❡ ✐❞❡❛❧

♠❡t❛✲♣r♦❣r❛♠♠✐♥❣✳

✇❡ ❛✐♠ ❢♦r ✐s ♥♦t ♠❡r❡❧② ❝♦rr❡❝t ♣r♦❣r❛♠s✱

❧✉r❦✐♥❣✖♠♦r❡ ❝♦♠♣❧❡① ❢❡❛t✉r❡s ❝❛♥ ✐♥❝r❡❛s❡

♥♦r ❡✈❡♥ ♣r♦✈❡♥ ❝♦rr❡❝t ♣r♦❣r❛♠s❀ ✇❡ ✇❛♥t

t❤❡ r✐s❦ ♦❢ ❜✉❣s✳

♣r♦♦❢ ❞♦♥❡ ❛❣❛✐♥st ❛ s♣❡❝✐✜❝❛t✐♦♥ t❤❛t ✐s ♥❛t✲

♠❡❝❤❛♥✐s♠s ✇❡ ❛❧s♦ ♥❡❡❞ ♥❡✇ ❝♦♠♣✉t❡r✲

✉r❛❧❧② ❡①♣r❡ss❡❞ ❢♦r ❛ ❞♦♠❛✐♥ ❡①♣❡rt✳

❛✐❞❡❞ s❛♥✐t② ❝❤❡❝❦s ♦❢ t❤❡ ♣r♦❣r❛♠ ❝♦❞❡✳

❚❤✐s ♣r♦❝❡ss ♦❢ r❡♣❧✐❝❛t✐♦♥ ✐s ♥♦t

♦♥❧② t❡❞✐♦✉s✱ ❜✉t ❡rr♦r✲♣r♦♥❡✱ ❜❡❝❛✉s❡ t❤❡
❍❡♥❝❡✱ ♦♥❡ ✐♠♣♦rt❛♥t tr❡♥❞

❲✐❞❡❧② ✉s❡❞ ♠♦❞❡r♥

❇✉t t❤❡r❡ ✐s ❛ ❞❛♥❣❡r
❲✐t❤ ♥❡✇ ❛❜str❛❝t✐♦♥

❈♦♥❝r❡t❡❧②✱ ✇❡ ❛✐♠ t♦ ✐❞❡♥t✐❢② ❝♦♠♠♦♥ ♣❛t✲
t❡r♥s ✐♥ t❤❡

s♣❡❝✐✜❝❛t✐♦♥

❚②♣❡s✳

♦❢ ♣r♦❣r❛♠s✱ ❛♥❞

❝❛♣t✉r❡ t❤♦s❡ ✐♥ ❧✐❜r❛r✐❡s✳ ❆t t❤❡ s❛♠❡ t✐♠❡✱
t❤❡ ♣❛tt❡r♥s ♦❢

✐♠♣❧❡♠❡♥t❛t✐♦♥s

❝♦♠♣✉t❡r s❝✐❡♥❝❡ t♦ ❦❡❡♣ s♦❢t✇❛r❡ ❢r♦♠ ❣♦✲

♦❢ t❤❡s❡

✐♥❣ ✇r♦♥❣✳

s♣❡❝✐✜❝❛t✐♦♥s ✇✐❧❧ ❛❧s♦ ❜❡ ❝❛♣t✉r❡❞ ✐♥ t❤❡

❝♦♠♣✉t❛t✐♦♥ ✐♥ ❛ ✇❛② t❤❛t ✐s ❝❤❡❝❦❛❜❧❡ ❜②

✇❛r❡ ✇✐❧❧ ❣♦ ❤❛♥❞✲✐♥✲❤❛♥❞ ✇✐t❤ ♣r♦♦❢s ♦❢ ✐ts

t❤❡ ❝♦♠♣✉t❡r ✐ts❡❧❢✳

❆s ❝❛s❡✲st✉❞✐❡s ✇❡

❚❤❡② ❛❝t ❛s ❝♦♥tr❛❝ts

❜❡t✇❡❡♥ t❤❡ ✐♠♣❧❡♠❡♥t❡r ♦❢ ❛ ♣r♦❣r❛♠ ♣❛rt

✇✐❧❧ ✇♦r❦ ✐♥ t❤r❡❡ ❛r❡❛s✿ ❞✐✈✐❞❡✲❛♥❞✲❝♦♥q✉❡r

❛♥❞ ✐ts ✉s❡rs✳

❛❧❣♦r✐t❤♠s✱ ❞♦♠❛✐♥ s♣❡❝✐✜❝ ♠♦❞❡❧❧✐♥❣ ❛♥❞

❚②♣❡✲❝❤❡❝❦✐♥❣ ❛t ❝♦♠♣✐❧❡

t✐♠❡ t❤❡♥ ❛♠♦✉♥ts t♦ ♣r♦✈✐♥❣ t❤❛t ♣r♦♣❡r✲

t❡st✐♥❣ t♦♦❧s✳

t✐❡s ❤♦❧❞ ❢♦r ❛❧❧ ❡①❡❝✉t✐♦♥s ♦❢ t❤❡ ♣r♦❣r❛♠✳
❇② t❤❡ ❈✉rr②✕❍♦✇❛r❞ ❝♦rr❡s♣♦♥❞❡♥❝❡✱ t②♣❡

✷ ❙✉r✈❡② ♦❢ t❤❡ ✜❡❧❞
❆❜str❛❝t✐♦♥✳

❚②♣❡s ❡♥❛❜❧❡ t❤❡ ♣r♦❣r❛♠♠❡r

t♦ ❦❡❡♣ tr❛❝❦ ♦❢ t❤❡ str✉❝t✉r❡ ♦❢ ❞❛t❛ ❛♥❞

❧✐❜r❛r②✱ s✉❝❤ t❤❛t t❤❡ ❞❡✈❡❧♦♣♠❡♥t ♦❢ s♦❢t✲
❢✉♥❝t✐♦♥❛❧ ❝♦rr❡❝t♥❡ss✳

❚②♣❡s ❛r❡ ✉s❡❞ ✐♥ ♠❛♥② ♣❛rts ♦❢

s②st❡♠s ❝❧♦s❡❧② ♠❛t❝❤ ✉♣ ✇✐t❤ ❧♦❣✐❝s✳ ❚②♣❡
s②st❡♠s ❢♦r ❧❛♥❣✉❛❣❡s ✇✐t❤ ❤✐❣❤❡r✲♦r❞❡r ❛❜✲
str❛❝t✐♦♥✱ ❝♦rr❡s♣♦♥❞ t♦ ❤✐❣❤❡r✲♦r❞❡r ❧♦❣✐❝s✳

❚❤❡ ❛❜✐❧✐t② t♦ ♥❛♠❡ ❛♥❞

❆ ✇❡❧❧✲❦♥♦✇ ❡①❛♠♣❧❡ ♦❢ ❛ s②st❡♠ ❜❛s❡❞ ♦♥

r❡✉s❡ ♣❛rts ♦❢ ❛❧❣♦r✐t❤♠s ✐s ♦♥❡ ♦❢ t❤❡ ❝♦r✲
♥❡rst♦♥❡s ♦❢ ❝♦♠♣✉t❡r s❝✐❡♥❝❡✳

t❤✐s ♣r✐♥❝✐♣❧❡ ✐s t❤❡ ❈♦q ♣r♦♦❢ ❛ss✐st❛♥t ❬✶❪✳

❆❜str❛❝t✲

✐♥❣ ♦✉t ❝♦♠♠♦♥ ♣❛tt❡r♥s ❡♥❛❜❧❡s s❡♣❛r❛✲
t✐♦♥ ♦❢ ❝♦♥❝❡r♥s✱ ❜♦t❤ ✐♥ t❤❡ s♠❛❧❧ ✭✈❛r✐✲

❉❡♣❡♥❞❡♥t❧② t②♣❡❞ ♣r♦❣r❛♠s✳

❛❜❧❡s✱

t❤♦✉❣❤ t②♣❡✲t❤❡♦r② ❤❛s ❜❡❡♥ ✉s❡❞ ❛s ❛ ❧♦❣✐❝

✉❧❡s✱

❢✉♥❝t✐♦♥s✮ ❛♥❞ ✐♥ t❤❡ ❧❛r❣❡ ✭♠♦❞✲
❧✐❜r❛r✐❡s✮✳

❈♦♥✈❡rs❡❧②✱

❊✈❡♥

❧❛❝❦ ♦❢ ❛❜✲

❢♦r ❞❡❝❛❞❡s✱ ✐t ❤❛s r❡❝❡♥t❧② ❣❛✐♥❡❞ ♣♦♣✉❧❛r✐t②

str❛❝t✐♦♥ ♠❛② ❢♦r❝❡ t❤❡ ✐♠♣❧❡♠❡♥t❛t✐♦♥ t♦

❛s ❛ ♠❡❞✐✉♠ ❢♦r ♣r♦❣r❛♠♠✐♥❣✳ ❚❤❡ ✢❛❣s❤✐♣

❝♦♥t❛✐♥ ♠✉❧t✐♣❧❡ ✐♥st❛♥❝❡s ♦❢ ❛ s✐♥❣❧❡ ♣❛t✲

♦❢ ❞❡♣❡♥❞❡♥t❧②✲t②♣❡❞ ♣r♦❣r❛♠s ✐s ♣❡r❤❛♣s

✶

❆♣♣❡♥❞✐① ❆

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❉❡♠❚❡❝❤✳❞❦ ♣r♦❥❡❝t✮✳

❈♦♠♣❝❡rt✱ ❛ ❈ ❝♦♠♣✐❧❡r ✇r✐tt❡♥ ❛♥❞ ✈❡r✐✲

❈r②♣t♦❣r❛♣❤② ✭s❡❡ t❤❡

✜❡❞ ✐♥ ❈♦q ❬✷❪✳

❖t❤❡r ❛♣♣❧✐❝❛t✐♦♥s ✐♥❝❧✉❞❡

■♥ ✐ts ❝✉rr❡♥t ✈❡rs✐♦♥✱ t❤❡ ♣❛rts ♦❢ t❤❡ ❆❣❞❛

✐♠♣❡r❛t✐✈❡ ♣r♦❣r❛♠s ✇✐t❤✐♥ ❈♦q✱ ❞❛t❛❜❛s❡

❧✐❜r❛r② ❛✐♠❡❞ ❛t ♣r♦❣r❛♠♠✐♥❣ ❛r❡ ❡ss❡♥t✐❛❧❧②

❛❝❝❡ss ✇✐t❤ st❛t✐❝ ❣✉❛r❛♥t❡❡s ❛♥❞ ❞✐str✐❜✉t❡❞

❞❡❝♦✉♣❧❡❞ ❢r♦♠ t❤❡ ♣❛rts ❛✐♠❡❞ ❛t ♣r♦✈✐♥❣✳

♣r♦❣r❛♠♠✐♥❣ ✇✐t❤ ❞❡♣❡♥❞❡♥t t②♣❡s ❬✸❪✳

❚❤✐s ❝❛♥ ❜❡ ❛ ❞r❛✇❜❛❝❦✿

t❤❡ str✉❝t✉r❡ ♦❢

❛ ♣r♦♦❢ ♦❢t❡♥ ❢♦❧❧♦✇s t❤❡ s❛♠❡ str✉❝t✉r❡ ❛s

❆❣❞❛✳

t❤❡ ♣r♦❣r❛♠ ✐t r❡❢❡rs t♦✱ t❤❡r❡❢♦r❡ ❦❡❡♣✐♥❣

❚❤❡ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥❣✉❛❣❡ ❆❣❞❛

t❤❡ t✇♦ s❡♣❛r❛t❡❞ ✈✐♦❧❛t❡s t❤❡ ♣r✐♥❝✐♣❧❡ ♦❢

✐s ❜❛s❡❞ ♦♥ ❍❛s❦❡❧❧ ❛♥❞ t②♣❡✲t❤❡♦r② ❬✹❪✳

❛❜str❛❝t✐♦♥ ❞❡s❝r✐❜❡❞ ❛❜♦✈❡✳

❲✐t❤✐♥ ✐t✱ ♦♥❡ ❝❛♥ ❡①♣r❡ss ♣r♦❣r❛♠s✱ ❢✉♥❝✲
t✐♦♥❛❧ s♣❡❝✐✜❝❛t✐♦♥s ❛s t②♣❡s✱ ❛♥❞ ♣r♦♦❢s ✭❢♦r

✸ Pr♦❣r❛♠♠❡ ❞❡s❝r✐♣t✐♦♥

❡①❛♠♣❧❡ ✉s✐♥❣ ❛❧❣❡❜r❛✐❝ r❡❛s♦♥✐♥❣✮ ✐♥ ❛ s✐♥✲
❣❧❡ ❧❛♥❣✉❛❣❡✳

❆❣❞❛ ✐s ❝✉rr❡♥t❧② ❡♠❡r❣✐♥❣

❛s ❛ ❧✐♥❣✉❛✲❢r❛♥❝❛ ♦❢ ♣r♦❣r❛♠♠✐♥❣ ✇✐t❤ ❞❡✲

❙t❛rt✐♥❣ ❢r♦♠ ♦✉r ❝✉rr❡♥t ❡①♣❡r✐❡♥❝❡ ✇✐t❤ ❧✐✲

♣❡♥❞❡♥t t②♣❡s ❛♥❞ ✐ts ❝❛♥♦♥✐❝❛❧ r❡❢❡r❡♥❝❡✱

❜r❛r✐❡s ❢♦r ❍❛s❦❡❧❧ ❛♥❞ ❆❣❞❛✱ ♦✉r ♣r♦❥❡❝t ✇✐❧❧

◆♦r❡❧❧✬s ❚❤❡s✐s ❬✺❪✱ ❤❛s ❜❡❡♥ ❝✐t❡❞ ✺✵ t✐♠❡s

❜❡ ♦r❣❛♥✐s❡❞ ✐♥ ♠✉❧t✐♣❧❡ ✐t❡r❛t✐♦♥s✱ ❡❛❝❤ r❡✲

♣❡r ②❡❛r s✐♥❝❡ ✐ts ♣✉❜❧✐❝❛t✐♦♥✳ ❚❤❡ ❢♦❝✉s ♦❢

✜♥✐♥❣ t❤❡ ❧✐❜r❛r✐❡s ♦❜t❛✐♥❡❞ ❞✉r✐♥❣ t❤❡ ♣r❡✲

t❤✐s ♣r♦❥❡❝t ✐s ♦♥ ❡①♣r❡ss✐♥❣ ❧✐❜r❛r✐❡s ♦❢ ❝♦r✲

✈✐♦✉s ♦♥❡✳ ❊❛❝❤ ✐t❡r❛t✐♦♥ ✇✐❧❧ ❤❛✈❡ t❤❡ ❢♦❧✲

r❡❝t ♣r♦❣r❛♠s ❛♥❞ ♣r♦♦❢s ✐♥ t❤❡ ❞❡♣❡♥❞❡♥t❧②

❧♦✇✐♥❣ t❤r❡❡ ♣❤❛s❡s✳

t②♣❡❞ ❢✉♥❝t✐♦♥❛❧ ❧❛♥❣✉❛❣❡ ♦❢ ❆❣❞❛✳

▲✐❜r❛r✐❡s ❢♦r ❞❡♣❡♥❞❡♥t t②♣❡s✳

✶✳ ❉❡✈❡❧♦♣♠❡♥t ♦❢ ❛ ♣r♦✈❡♥✲❝♦rr❡❝t
❛♣♣❧✐❝❛t✐♦♥ ✐♥ ❛ ❣✐✈❡♥ ❞♦♠❛✐♥✳ ❲❡ ❜❡✲

❆❣❞❛

❛♥❞ ❈♦q ❝♦♠❡ ✇✐t❤ st❛♥❞❛r❞ ❧✐❜r❛r✐❡s t❤❛t

❧✐❡✈❡ t❤❛t t❤❡ ❜❡st ✇❛② t♦ ❞❡✈❡❧♦♣ ❧✐❜r❛r✐❡s

❝♦♥t❛✐♥ ✉s❡❢✉❧ ❜✉✐❧❞✐♥❣ ❜❧♦❝❦s t♦ ❝r❡❛t❡ ♣r♦✲

✐s ❜② ❛❜str❛❝t✐♥❣ ❝♦♠♠♦♥ ♣❛tt❡r♥s ❢♦✉♥❞ ✐♥

❣r❛♠s✱ s♣❡❝✐✜❝❛t✐♦♥s✱ ❛♥❞ ♣r♦♦❢s✳ ❚❤❡ ❈♦q

✈❛r✐♦✉s ❛♣♣❧✐❝❛t✐♦♥ ❞♦♠❛✐♥s✳ ■♥ t❤✐s ♣❤❛s❡✱

❧✐❜r❛r② ✐s ♣❛rt ♦❢ ❛ ♠❛t✉r❡ s②st❡♠ ✇❤✐❝❤ ❤❛s

✇❡ ✇✐❧❧ ❛ss❡ss t❤❡ ✈✐❛❜✐❧✐t② ♦❢ ♦✉r ❧✐❜r❛r✐❡s ❜②

❜❡❡♥ ✉s❡❞ ✐♥ ♠❛♥② ♣r♦❥❡❝ts✳

❛♣♣❧②✐♥❣ t❤❡♠ t♦ ❛ ♣❛rt✐❝✉❧❛r ❞♦♠❛✐♥✳

❍♦✇❡✈❡r✱ ✐t

✐s ♠♦st❧② ❛♣♣❧✐❡❞ t♦ ♣r♦♦❢s r❛t❤❡r t❤❛♥ ♣r♦✲

✷✳ ❊①tr❛❝t✐♦♥ ♦❢ ❝♦♠♠♦♥ ♣❛tt❡r♥s ✐♥t♦
❧✐❜r❛r✐❡s✳ ◆❡①t✱ ✇❡ ✇✐❧❧ ✐❞❡♥t✐❢② ❝♦♠♠♦♥

❣r❛♠s✱ ❜❡❝❛✉s❡ t❤❡ ❈♦q s②st❡♠ ✐s ♠♦st❧② ✐♥✲
t❡♥❞❡❞ ❛s ❛ ♣r♦♦❢ ❛ss✐st❛♥t r❛t❤❡r t❤❛♥ ❛ ♣r♦✲
❣r❛♠♠✐♥❣ ❧❛♥❣✉❛❣❡✳

❊✈❡♥ ♣r♦❥❡❝ts ✇❤✐❝❤

♣❛tt❡r♥s ❢♦✉♥❞ ✐♥ t❤❡ ♣r♦❣r❛♠s ❛♥❞ s♣❡❝✐✜✲

❛✐♠ t♦ ✉s❡ ❈♦q ❛s ❛ ♣r♦❣r❛♠♠✐♥❣ ♣❧❛t❢♦r♠✱

❝❛t✐♦♥s ♣r♦❞✉❝❡❞ ❛❜♦✈❡✱ ❛♥❞ ❝❛♣t✉r❡ t❤❡♠

s✉❝❤ ❛s ❨♥♦t ❛♥❞ ❈♦♠♣❝❡rt ❬✷✱ ✻❪ r❡t❛✐♥ t❤✐s
s❡♣❛r❛t✐♦♥✳

✐♥ ❧✐❜r❛r✐❡s✳ ❆t t❤❡ s❛♠❡ t✐♠❡✱ ✇❡ ✇✐❧❧ r❡❢❛❝✲

❚❤❡ s❛♠❡ ♦❜s❡r✈❛t✐♦♥ ❛♣♣❧✐❡s

t♦r t❤❡ ❛♣♣❧✐❝❛t✐♦♥ ❛♥❞ t✐❡ ❡❛❝❤ s♣❡❝✐✜❝❛t✐♦♥

t♦ t❤❡ ❧✐❜r❛r✐❡s ♦❢ ♠♦st s②st❡♠s ✇✐t❤ ❞❡♣❡♥✲

♣❛tt❡r♥ t♦ ❛♥ ✐♠♣❧❡♠❡♥t❛t✐♦♥ ♣❛tt❡r♥✳

❞❡♥t t②♣❡s✳ ❚❤❡ ❆❣❞❛ st❛♥❞❛r❞ ❧✐❜r❛r② ✭❞❡✲

✸✳ ❘❡✜♥✐♥❣ t❤❡ ♣r♦❣✳ ❧❛♥❣✉❛❣❡✳

✈❡❧♦♣❡❞ ♠❛✐♥❧② ❜② ❉❛♥✐❡❧ss♦♥✮✱ ❤❛s ❡✈♦❧✈❡❞
❢r♦♠ ❝♦♠♠♦♥ ❛❜str❛❝t✐♦♥s ♥❡❡❞❡❞ ❜② ❆❣❞❛
♣r♦❣r❛♠♠❡rs✳

♣❤❛s❡ ✇❡ ✇✐❧❧ ❛ss❡ss t❤❡ str♦♥❣ ❛♥❞ ✇❡❛❦

■t ❤❛s ❜❡❡♥ ❛♣♣❧✐❡❞ t♦ s❡✈✲

♣♦✐♥ts ♦❢ t❤❡ ✉♥❞❡r❧②✐♥❣ ♣r♦❣r❛♠♠✐♥❣ ❡♥✈✐✲

❡r❛❧ ❞♦♠❛✐♥s✱ ✐♥ ♣❛rt✐❝✉❧❛r ♣❛rs❡r ❝♦♠❜✐♥❛✲
t♦rs ❬✼❪✱ ❆❧❣❡❜r❛ ♦❢ Pr♦❣r❛♠♠✐♥❣ ❬❏✶✾❪

✶ ❲❡

✶

■♥ t❤✐s

r♦♥♠❡♥t ✇❡ ✉s❡✳ ❲❡ ✇✐❧❧ ✐♥❢♦r♠ t❤❡ ❣r♦✉♣

❛♥❞

✐♥ ❝❤❛r❣❡ ♦❢ t❤❡ ❞❡✈❡❧♦♣♠❡♥t ♦❢ t❤❡ t♦♦❧ ♦❢
t❤❡ ♣♦ss✐❜❧❡ s❤♦rt❝♦♠✐♥❣s ✇❡ ♠✐❣❤t ✐❞❡♥t✐❢②✱

✉s❡ ❬❏♥♥❪ t♦ ❝✐t❡ ♣❛♣❡rs ✐♥ ❏❛♥ss♦♥✬s ♣✉❜❧✐✲

❛♥❞ ♣❛rt✐❝✐♣❛t❡ ✐♥ t❤❡✐r r❡♠❡❞②✱ ✐❢ s✉✐t❛❜❧❡✳

❝❛t✐♦♥ ❧✐st ✭❛♣♣❡♥❞✐① ❈✮ t♦ ❛✈♦✐❞ ❞✉♣❧✐❝❛t✐♦♥✳

✷

❆♣♣❡♥❞✐① ❆

✸✳✶

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❉♦♠❛✐♥ s♣❡❝✐✜❝ ♠♦❞❡❧❧✐♥❣✿

❆♣♣❧✐❝❛t✐♦♥ ❛r❡❛s

✐s ♣r♦♦❢ ♦❢ ❝♦rr❡❝t♥❡ss ✐s ✐❢ ♥♦✲♦♥❡ ✉♥❞❡r✲

❲❡ ✇♦r❦ ✐t❡r❛t✐✈❡❧② ♦♥ ❝❛s❡ st✉❞✐❡s ✭❝♦rr❡❝t

st❛♥❞s t❤❡ s♣❡❝✐✜❝❛t✐♦♥❄ ❲❡ t❛❦❡ t❤❡ st❛♥❝❡

❧✐❜r❛r✐❡s✮ ✐♥ t❤r❡❡ ❛♣♣❧✐❝❛t✐♦♥ ❛r❡❛s✿

❆❧❣❡❜r❛ ♦❢ P❛r❛❧❧❡❧ Pr♦❣r❛♠♠✐♥❣✿

❲❤❛t ❣♦♦❞

t❤❛t s♣❡❝✐✜❝❛t✐♦♥s ♠✉st ❜❡ r❡❛❞✐❧② ✉♥❞❡r✲
st♦♦❞ ❜② ❞♦♠❛✐♥ ❡①♣❡rts✱ ❛♥❞ t❤❡r❡❢♦r❡ ✐t
❆

✐s ✐♠♣♦rt❛♥t ❢♦r ❝♦♠♣✉t❡r✲s❝✐❡♥t✐sts t♦ ✇♦r❦

❧❛r❣❡ ❝❧❛ss ♦❢ s❡q✉❡♥❝❡✲♣r♦❝❡ss✐♥❣ ❛❧❣♦r✐t❤♠s

✇✐t❤ t❤❡ ❞♦♠❛✐♥ s♣❡❝✐✜❝ ❝♦♥❝❡♣ts✳ ❲❡ ❤❛✈❡

❝❛♥ ❜❡ ❝♦♥✈❡rt❡❞ t♦ ♣❛r❛❧❧❡❧ ❛❧❣♦r✐t❤♠s ✐❢

❞♦♥❡ s♦ ✐♥ t❤❡ ♣❛st✱ ✐♥ t❤❡ ❞♦♠❛✐♥ ♦❢ ✈✉❧♥❡r❛✲

t❤❡② ❛r❡ ♠♦♥♦✐❞ ❤♦♠♦♠♦r♣❤✐s♠s✳ ❚❤❛t ✐s✱

❜✐❧✐t② ❢♦r ❝❧✐♠❛t❡ ✐♠♣❛❝t ❬❏✶✼❪✱ ❣r❛♠♠❛rs ❢♦r

❛ ❢✉♥❝t✐♦♥

f : A → B

❝❛♥ ❜❡ ♣❛r❛❧❧❡❧✐s❡❞

❧❛♥❣✉❛❣❡ ♣r♦❝❡ss✐♥❣ ❬❏✶✸❪✱ ❛♥❞ ♠❛t❤❡♠❛t✐✲

✐❢ ✐t s❛t✐s✜❡s t❤❡ ❢♦❧❧♦✇✐♥❣ ❧❛✇s✿

❝❛❧ ❡❝♦♥♦♠✐❝s ❬❏✾❪✳

f empty A
= empty B
f (a +
+A b) = f a +
+B f b
✇❤❡r❡

empty

❛♥❞

❛♥❞ ❝♦♠♣♦s✐t✐♦♥✳

+
+

■♥ ❛❞❞✐t✐♦♥ t♦ ❞♦♠❛✐♥

❦♥♦✇❧❡❞❣❡ t❤✐s r❡q✉✐r❡s s✉♣♣♦rt ❢♦r ❤✐❣❤❡r✲
♦r❞❡r ❝♦♥str✉❝t✐♦♥s ❧✐❦❡ ♠♦♥❛❞s✱
❛♥❞ ♥❛t✉r❛❧ tr❛♥s❢♦r♠❛t✐♦♥s✳

❢✉♥❝t♦rs

■♥ t❤✐s ♣❛rt

✇❡ ✇✐❧❧ ❢♦❝✉s ♦♥ ♦♣t✐♠✐s❛t✐♦♥ ❛♥❞ ❞②♥❛♠✐❝❛❧

❞❡♥♦t❡ ♠♦♥♦✐❞❛❧ ✉♥✐t

s②st❡♠s✳ ■♥ ♣❛rt✐❝✉❧❛r✱ ✇❡ ✇✐❧❧ ❝♦♥t✐♥✉❡ t❤❡

■♥ s♦♠❡ ❝❛s❡s✱ t❤❡ ❢✉♥❝✲

✇♦r❦ ♦♥ ❡❝♦♥♦♠✐❝s ❛♥❞ ❞❡✈❡❧♦♣ ❧✐❜r❛r✐❡s ♦❢

t✐♦♥ ✐s ♥♦t ❛ ♠♦♥♦✐❞ ❤♦♠♦♠♦r♣❤✐s♠✱ ❜✉t ✐t

s♣❡❝✐✜❝❛t✐♦♥s ❢♦r ❛❣❡♥t✲❜❛s❡❞ ♠♦❞❡❧❧✐♥❣✳ ❲❡

❝❛♥ ❜❡ ♣❤r❛s❡❞ ✐♥ t❡r♠s ♦❢ ❛♥ ❛✉①✐❧✐❛r② ❢✉♥❝✲

✇✐❧❧ ❛❧s♦ ✇♦r❦ ♦♥ ✐♠♣r♦✈✐♥❣ ❧❛♥❣✉❛❣❡ s✉♣✲

t✐♦♥✱ ✇❤✐❝❤ ✇♦r❦s ♦♥ ❛♥ ❡①t❡♥❞❡❞ t②♣❡✳

♣♦rt t♦ ♣r❡s❡♥t t❤❡ s♣❡❝✐✜❝❛t✐♦♥s ✐♥ ❛ ✇❛②

❆ s✐♠♣❧❡ ❡①❛♠♣❧❡ ✐s ✇♦r❞ ❝♦✉♥t✐♥❣✱ ✇❤✐❝❤

❛❝❝❡ss✐❜❧❡ t♦ t❤❡ ❞♦♠❛✐♥ ❡①♣❡rts✳

♠❛♣s ❡❛❝❤ str✐♥❣ t♦ ❛ ♥❛t✉r❛❧ ♥✉♠❜❡r ✭t❤❡
♥✉♠❜❡r ♦❢ ✇❤✐t❡✲s♣❛❝❡ s❡♣❛r❛t❡❞ ✇♦r❞s ✐♥
t❤❡ str✐♥❣✮✳

❚❡st✐♥❣ ❚♦♦❧s✿

❲♦r❞ ❝♦✉♥t✐♥❣ ✐s ♥♦t ❜② ✐ts❡❧❢

❛ ♠♦♥♦✐❞ ❤♦♠♦♠♦r♣❤✐s♠ ❜✉t ✐❢ ✇❡ ❦❡❡♣ t❤❡

✜❞❡♥❝❡ ✐♥ ♣r♦❣r❛♠ ❝♦rr❡❝t♥❡ss✳ ❆s ✐t ✐s ✇❡❧❧

❛❜♦✉t s♣❛❝✐♥❣ ♦♥ ❡✐t❤❡r s✐❞❡ ✇❡ ❝❛♥ ♠❛❦❡ ❛

❦♥♦✇♥✱ t❡st✐♥❣ ❝❛♥♥♦t s❤♦✇ t❤❡ ❛❜s❡♥❝❡ ♦❢

helper ✳

helper
countSpaces
...
wordCount
wordCount

t❡st✐♥❣

t♦♦❧s ❤❛✈❡ ♣r♦✈❡❞ ✉s❡❢✉❧ t♦ ✐♠♣r♦✈❡ t❤❡ ❝♦♥✲

♥✉♠❜❡r ♦❢ ❢✉❧❧ ✇♦r❞s✱ ♣❧✉s s♦♠❡ ✐♥❢♦r♠❛t✐♦♥
❤♦♠♦♠♦r♣❤✐❝

Pr♦♣❡rt②✲❜❛s❡❞

❜✉❣s✱ ♦♥❧② t❤❡✐r ♣r❡s❡♥❝❡✳ ❇✉t ✐s ✐t ♣♦ss✐❜❧❡

: String → (Count, Spa)
: (Count, Spa) → N

t♦ q✉❛♥t✐❢② t❤❡ ❝♦♥✜❞❡♥❝❡ ❣❛✐♥❡❞ ❜② r✉♥♥✐♥❣

: String → N
= countSpaces ◦ helper

❞✐r❡❝t✐♦♥ ✐s t♦ s♣❡❝✐❢② t❤❡ s❡t ♦❢ ✐♥♣✉ts ❝♦✈✲

❛ t❡st s✉✐t❡❄ ❲❡ ❛✐♠ t♦ ❣✐✈❡ ❛ ♣♦s✐t✐✈❡ ❛♥✲
s✇❡r t♦ t❤❡ q✉❡st✐♦♥✳

❆ ✜rst st❡♣ ✐♥ t❤✐s

❡r❡❞ ❜② ❛ t❡st✲s✉✐t❡✳ ■♥ t❤✐s ♣r♦❥❡❝t ✇❡ ✇✐❧❧
❢♦❝✉s ♦♥ ❧❛r❣❡ ❛❜str❛❝t s②♥t❛① tr❡❡ ✭❆❙❚✮

❚❤❡ r❡s✉❧t✐♥❣ ❛❧❣♦r✐t❤♠ ✇♦r❦s ❢♦r ❛♥② tr❡❡✲

t②♣❡s t②♣✐❝❛❧❧② ✉s❡❞ ✐♥ ❝♦♠♣✐❧❡rs✱ ❛♥❞ ❛✐♠

❧✐❦❡ ♣❛rt✐t✐♦♥✐♥❣ ♦❢ t❤❡ str✐♥❣ ✐♥t♦ ❝❤✉♥❦s

❛t s✉♣♣♦rt✐♥❣ ✐♥t❡r❡st✐♥❣ s✉❜s❡ts ❧✐❦❡ ✇❡❧❧✲

❛♥❞ ❝❛♥ t❤✉s ❜❡ ♠❛❞❡ ❢❛st ❜② ✉s✐♥❣ ♠❛♥②

t②♣❡❞ t❡r♠s ♦r ❜❛❧❛♥❝❡❞ tr❡❡s ✭❡①♣r❡ss✐❜❧❡

♣r♦❝❡ss♦rs✳

❛s ✐♥❞✉❝t✐✈❡ ❢❛♠✐❧✐❡s ✐♥ ❆❣❞❛✮✳

■♥ t❤✐s ♣r♦❥❡❝t ✇❡ ✇❛♥t t♦ ❞❡✲

✈❡❧♦♣ ❛ ❧✐❜r❛r② ❢♦r s♣❡❝✐❢②✐♥❣✱ ✐♠♣❧❡♠❡♥t✲

■♥ ❛ r❡❝❡♥t ♣❛♣❡r ❬❏✶✶❪ ✇❡ ♣r❡s❡♥t❡❞ ❛ t❤❡♦r②

✐♥❣ ❛♥❞ ♣r♦✈✐♥❣ ❝♦rr❡❝t♥❡ss ♦❢ ❞✐✈✐❞❡✲❛♥❞✲

❢♦r s♣❡❝✐❢②✐♥❣✱ ❛♥❞ ❛ ❣❡♥❡r✐❝ ❍❛s❦❡❧❧ ❧✐❜r❛r②

❝♦♥q✉❡r ❛❧❣♦r✐t❤♠s✳

■♥✐t✐❛❧ r❡s✉❧ts ❜② ♦✉r

❢♦r ❡✣❝✐❡♥t❧② ❡♥✉♠❡r❛t✐♥❣✱ t❤❡ t❡r♠s ♦❢ ❝♦♠✲

❣r♦✉♣ s❤♦✇ t❤❛t t❤✐s ✇♦r❦s ❡✈❡♥ ❢♦r s♦♠❡✲

♣❧❡① ❆❙❚✲t②♣❡s✳ ❚❤❡ ♣r✐♠❛r② ❛♣♣❧✐❝❛t✐♦♥ ✐s

t❤✐♥❣ ❛s s❡q✉❡♥t✐❛❧✲❧♦♦❦✐♥❣ ❛s ♣❛rs✐♥❣ ❬✽❪✳

♣r♦♣❡rt②✲❜❛s❡❞ t❡st✐♥❣✱ ✇❤❡r❡ ✐t ✐s ✉s❡❞ t♦

✸

❆♣♣❡♥❞✐① ❆

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❞❡✜♥❡ ❜♦t❤ r❛♥❞♦♠ s❛♠♣❧✐♥❣ ✭◗✉✐❝❦❈❤❡❝❦

❣r❛♠s ❛♥❞ ♣r♦♦❢s ✐♥ t❤❡ ❆❧❣❡❜r❛ ♦❢ Pr♦❣r❛♠✲

❣❡♥❡r❛t♦rs✮ ❛♥❞ ❡①❤❛✉st✐✈❡ ❡♥✉♠❡r❛t✐♦♥✳ ■♥

♠✐♥❣ ❬❏✷✱ ❏✶✾❪ tr❛❞✐t✐♦♥✳

t❤✐s ♣r♦❥❡❝t ✇❡ ✇✐❧❧ ♣♦rt t❤✐s ❧✐❜r❛r② ❛♥❞

❝❧✉❞❡s ❛♥ ❡✣❝✐❡♥t s♣❛rs❡ ♠❛tr✐① ❜❛s❡❞ ❛❧❣♦✲

✐ts s♣❡❝✐✜❝❛t✐♦♥ t♦ ❆❣❞❛ ❛♥❞ ❡①t❡♥❞ ✐t t♦✲

r✐t❤♠ ❢♦r ♣❛r❛❧❧❡❧ ♣❛rs✐♥❣ ❛♥❞ ✐ts ♣r♦♦❢ ❬✽❪✳

✇❛r❞s ✐♥❞✉❝t✐✈❡ ❢❛♠✐❧✐❡s✳ ❖✉r ❤②♣♦t❤❡s✐s ✐s

❘❡❝❡♥t ✇♦r❦ ✐♥✲

t❤❛t✱ ❝♦♠♣❛r❡❞ t♦ ◗✉✐❝❦❈❤❡❝❦✱ t❤❡ ♠♦r❡ ❛❧✲

❉♦♠❛✐♥ ❙♣❡❝✐✜❝ ▼♦❞❡❧❧✐♥❣✿

❣❡❜r❛✐❝ ❡♥✉♠❡r❛t✐♦♥ ❛♣♣r♦❛❝❤ ✇✐❧❧ ❜❡ ❡❛s✐❡r

❞❡♥t t②♣❡ t❤❡♦r② ✐s r✐❝❤ ❡♥♦✉❣❤ t♦ ❡①♣r❡ss

t♦ s♣❡❝✐❢② ❛♥❞ ♣r♦✈❡ ❝♦rr❡❝t✳

t❤❛t ❛ ♣r♦❣r❛♠ s❛t✐s✜❡s ❛ ❢✉♥❝t✐♦♥❛❧ s♣❡❝✐✲
✜❝❛t✐♦♥✱ ❜✉t t❤❡r❡ ✐s ♥♦

✹ Pr❡❧✐♠✐♥❛r② ✜♥❞✐♥❣s

♠❡t❤♦❞ t♦

❞❡r✐✈❡ ❛ ♣r♦❣r❛♠ ♦♥❝❡ t❤❡ s♣❡❝✐✜❝❛t✐♦♥✲❛s✲
t②♣❡ ✐s ✇r✐tt❡♥✳ ❖♥ t❤❡ ♦t❤❡r ❤❛♥❞✱ ❇✐r❞ ✫
❞❡ ▼♦♦r ❬✶✹❪ ❣✐✈❡ ❛ ❣❡♥❡r❛❧ ♠❡t❤♦❞♦❧♦❣② t♦

❲❡ ❤❛✈❡ ♣✉❜❧✐s❤❡❞ ✐♥✐t✐❛❧ r❡s✉❧ts ✐♥ ❛❧❧ t❤❡

❞❡r✐✈❡ ❍❛s❦❡❧❧ ♣r♦❣r❛♠s ❢r♦♠ s♣❡❝✐✜❝❛t✐♦♥s✱

t❤r❡❡ s✉❣❣❡st❡❞ ✐t❡r❛t✐♦♥ ♣❤❛s❡s ❛♥❞ t❤r❡❡

✈✐❛ ❛❧❣❡❜r❛✐❝ r❡❛s♦♥✐♥❣✳ ❉❡s♣✐t❡ t❤❡ str♦♥❣

❛♣♣❧✐❝❛t✐♦♥ ❛r❡❛s ❛s ✐♥❞✐❝❛t❡❞ ❜❡❧♦✇✳

Pr♦✈❡♥✲❝♦rr❡❝t ❛♣♣❧✐❝❛t✐♦♥s✿

❛✲♣r✐♦r✐

❉❡♣❡♥✲

❡♠♣❤❛s✐s ♦♥ ❝♦rr❡❝t♥❡ss✱ t❤❡✐r s♣❡❝✐✜❝❛t✐♦♥s
❲❡ ❤❛✈❡

❛♥❞ ♣r♦♦❢s ❛r❡ ♥♦t ❡①♣r❡ss❡❞ ✐♥ ❛ ❢♦r♠❛❧❧②

✇♦r❦❡❞ ♦♥ ❝♦rr❡❝t ❛♣♣❧✐❝❛t✐♦♥s ✐♥ ❍❛s❦❡❧❧ ❬✾❪

❝❤❡❝❦❛❜❧❡ ✇❛②✳

❬❏✺❪ ❛♥❞ s✉♣♣♦rt✐♥❣ t❤❡♦r② ❬❏✷✶❪✳

■♥ ❬❏✽❪ ✇❡ ❤❛✈❡ s❤♦✇♥ ❤♦✇

❲❡ ❤❛✈❡

t♦ ❡♥❝♦❞❡ ♣r♦❣r❛♠ ❞❡r✐✈❛t✐♦♥ ✐♥ t❤❡ st②❧❡

❛❧s♦ ✇♦r❦❡❞ ♦♥ ❛♣♣❧✐❝❛t✐♦♥s t♦ ❝❧✐♠❛t❡ ✐♠✲

♦❢ ❇✐r❞ ❛♥❞ ❞❡ ▼♦♦r✱ ✐♥ ❆❣❞❛✳ ❆ ♣r♦❣r❛♠

♣❛❝t r❡s❡❛r❝❤ ❛♥❞ ❡❝♦♥♦♠✐❝ ♠♦❞❡❧❧✐♥❣ ❞✐✲

✐s ❝♦✉♣❧❡❞ ✇✐t❤ ❛♥ ❛❧❣❡❜r❛✐❝ ❞❡r✐✈❛t✐♦♥ ❢r♦♠

r❡❝t❧② ✐♥ ❆❣❞❛ ❬❏✾✱ ❏✶✵❪✳

❛ s♣❡❝✐✜❝❛t✐♦♥✱ ✇❤♦s❡ ❝♦rr❡❝t♥❡ss ✐s ❣✉❛r❛♥✲

P❛tt❡r♥s ✐♥t♦ ❧✐❜r❛r✐❡s✿

t❡❡❞ ❜② t❤❡ t②♣❡ s②st❡♠✳ ■♥ t❤✐s ♣r♦❥❡❝t ✇❡

❲❡ ❤❛✈❡ ❞❡✈❡❧✲

✇❛♥t t♦ ❣♦ ❢✉rt❤❡r ✐♥ t❤✐s ❞✐r❡❝t✐♦♥ ❛♥❞ ❞❡✲

♦♣❡❞✱ ✐♠♣❧❡♠❡♥t❡❞ ❛♥❞ ❝♦♠♣❛r❡❞ ❧✐❜r❛r✐❡s
♦❢ ❣❡♥❡r✐❝ ❢✉♥❝t✐♦♥s ❬✶✵✱ ✶✶❪ ❬❏✶✻❪✳

✈❡❧♦♣ ✉s❡❢✉❧ ❧✐❜r❛r✐❡s ♦❢ ♣r♦❣r❛♠s ❛♥❞ ♣r♦♦❢s

▼♦st

✇✐t❤ ❝♦rr❡s♣♦♥❞✐♥❣ t②♣❡s ❛♥❞ t❤❡♦r❡♠s✳

♦❢ t❤✐s ❤❛s ❜❡❡♥ ❞♦♥❡ ✐♥ ❍❛s❦❡❧❧✱ ❜✉t ✐t

❚❡st✐♥❣ ❛♥❞ ✈❡r✐✜❝❛t✐♦♥✿

❤❛s ❜❡❝♦♠❡ ❝❧❡❛r t❤❛t t❤❡ ♥❛t✉r❛❧ s❡tt✐♥❣
❢♦r ❣❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣ ✐s ❞❡♣❡♥❞❡♥t t②♣❡s✳

❲❡ ❤❛✈❡ ❡①✲

♣❧♦r❡❞ t❤❡ t❡♥s✐♦♥ ❜❡t✇❡❡♥ t❡st✐♥❣ ❛♥❞ ♣r♦✈✲

❲❡ ❤❛✈❡ ❛❧s♦ ✇♦r❦❡❞ ♦♥ ❧✐❜r❛r✐❡s ❢♦r ♣❛rs✐♥❣

✐♥❣ ♦❢ ❤✐❣❤❡r✲♦r❞❡r ♣r♦♣❡rt✐❡s ❬❏✷✵✱ ❏✶✵❪✱ ❞❡✲

❬✶✷❪ ❬❏✶✸❪✱ t❡st✐♥❣ ❬❏✶✶✱ ❏✶✷❪ ❛♥❞ t❤❡ ❛❜♦✈❡

✈❡❧♦♣❡❞ ❛ t❡❝❤♥✐q✉❡ ❢♦r ❞r❛st✐❝❛❧❧② r❡❞✉❝✐♥❣

♠❡♥t✐♦♥❡❞ ❛♣♣❧✐❝❛t✐♦♥s t♦ ❝❧✐♠❛t❡ ❛♥❞ ❡❝♦♥✲

t❤❡ ♥✉♠❜❡r ♦❢ t❡sts r❡q✉✐r❡❞ ❢♦r ♣♦❧②♠♦r✲

♦♠②✳

♣❤✐❝ ♣r♦♣❡rt✐❡s ❬❏✶✺❪✱ ❞❡✈❡❧♦♣❡❞ ❛ ❧✐❜r❛r② ❢♦r

❘❡✜♥❡♠❡♥t ♦❢ ♣r♦❣✳ ❧❛♥❣✉❛❣❡s✿

s♣❡❝✐❢②✐♥❣ ❛♥❞ t❡st✐♥❣ ❝❧❛ss ❧❛✇s ❬❏✶✷❪ ❛♥❞ ❛

❲❡

❧✐❜r❛r② ❢♦r ❡♥✉♠❡r❛t✐♥❣ t❡st ❝❛s❡s ❬❏✶✶❪✳

❤❛✈❡ ❞❡s✐❣♥❡❞ ❛ ❣❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥✲

❲❡ ❤❛✈❡ ❛❧s♦ st❛rt❡❞ ❛ ✈❡r② ♣r♦♠✐s✐♥❣ ❧✐♥❡ ♦❢

❣✉❛❣❡ ❡①t❡♥s✐♦♥ ✭P♦❧②P ❬❏✶❪✮ ❢♦r ❍❛s❦❡❧❧✱ ❛♥❞

✇♦r❦ ♦♥

✇❡ ❛r❡ ❛❝t✐✈❡❧② ✐♥✈♦❧✈❡❞ ✐♥ t❤❡ ❞❡s✐❣♥ ♦❢ t❤❡
❆❣❞❛ ❧❛♥❣✉❛❣❡ ❬❏✸✵❪ ❬✶✸❪✳ ❲❡ ❤❛✈❡ ❛❧s♦ ❜❡❡♥

✐♥ ❬❏✶✹✱ ❏✻❪ ✇❡

✏❚❤❡♦r❡♠s ❢♦r ❢r❡❡✦✑ ❬✶✺❪ ❝❛♥ ❜❡ ❡①t❡♥❞❡❞ t♦

✐♥✈♦❧✈❡❞ ✐♥ t❤❡ ❞❡✈❡❧♦♣♠❡♥t ♦❢ t❤❡ ❈♦♥❝❡♣ts

❞❡♣❡♥❞❡♥t❧② t②♣❡❞ ❧❛♥❣✉❛❣❡s t♦ ❣✐✈❡ ✏Pr♦♦❢s

❢❡❛t✉r❡ ❛✐♠❡❞ ❛t ✐♠♣r♦✈✐♥❣ ❢✉t✉r❡ ✈❡rs✐♦♥s

❢♦r ❢r❡❡✑✳

♦❢ ❈✰✰ ❛♥❞ ❍❛s❦❡❧❧ ❬❏✼✱ ❏✶✽❪✳

❆❧❣❡❜r❛ ♦❢ P❛r❛❧❧❡❧ Pr♦❣r❛♠♠✐♥❣✿

♣❛r❛♠❡tr✐❝✐t② t❤❡♦r② ✿

❤❛✈❡ ❡①♣❧❛✐♥❡❞ ❤♦✇ t❤❡ ❝❧❛ss✐❝ r❡s✉❧ts ❢r♦♠

❇② ❝♦♠❜✐♥✐♥❣ ♦✉r r❡s✉❧ts ❢r♦♠

♣♦❧②♠♦r♣❤✐❝ t❡st✐♥❣ ✇✐t❤ ♦✉r ❧❛t❡r r❡s✉❧ts ♦♥
❲❡

♣❛r❛♠❡tr✐❝✐t② ✇❡ ❛✐♠ ❛t ❛ ❣❡♥❡r✐❝ ❧✐❜r❛r② ❢♦r

❤❛✈❡ ✇♦r❦❡❞ ❛❝t✐✈❡❧② ♦♥ ✐♠♣❧❡♠❡♥t✐♥❣ ♣r♦✲

t❡st✐♥❣ ♣♦❧②♠♦r♣❤✐❝ ♣r♦♣❡rt✐❡s ✐♥ ❆❣❞❛✳

✹

❆♣♣❡♥❞✐① ❆

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

✺ ❙✐❣♥✐✜❝❛♥❝❡

❘❡❢❡r❡♥❝❡s
❬✶❪ ❚❤❡ ❈♦q ❞❡✈❡❧♦♣♠❡♥t t❡❛♠✳ ❚❤❡ ❈♦q ♣r♦♦❢
❛ss✐st❛♥t✱ ✷✵✶✵✳

❊✛❡❝t✐✈❡ ♣r♦❞✉❝t✐♦♥ ♦❢ ❝♦rr❡❝t s♦❢t✇❛r❡ ✐s

❬✷❪ ▲❡r♦②✳ ❋♦r♠❛❧ ✈❡r✐✜❝❛t✐♦♥ ♦❢ ❛ r❡❛❧✐st✐❝
❝♦♠♣✐❧❡r✳ ❈♦♠♠✳ ♦❢ t❤❡ ❆❈▼✱ ✺✷✭✼✮✿✶✵✼✕
✶✶✺✱ ✷✵✵✾✳

❛ ♣r♦❜❧❡♠ ✇❤✐❝❤ r❡♠❛✐♥s ✉♥s♦❧✈❡❞✱ ❛♥❞ ✐s
♦❢ ❣r❡❛t ❡❝♦♥♦♠✐❝ s✐❣♥✐✜❝❛♥❝❡✳
❞❡♣❡♥❞❡♥t❧②✲t②♣❡❞ ❧❛♥❣✉❛❣❡s✱

❇② ✉s✐♥❣

t❤✐s ♣r♦❥❡❝t

❛✐♠s t♦ r❡❞✉❝❡ t❤❡ ♣♦t❡♥t✐❛❧ ❢♦r ❡rr♦rs ❜②

❬✸❪ ❙✇❛♠② ❡t ❛❧✳ ❙❡❝✉r❡ ❞✐str✐❜✉t❡❞ ♣r♦❣r❛♠✲
♠✐♥❣ ✇✐t❤ ✈❛❧✉❡✲❞❡♣❡♥❞❡♥t t②♣❡s✳ ■♥ ■❈❋P
✷✵✶✶✱ ♣✳ ✷✻✻✳

❞❡✈❡❧♦♣✐♥❣ t❤❡ s♣❡❝✐✜❝❛t✐♦♥ ♦❢ ❛ s②st❡♠ t♦✲
❣❡t❤❡r ✇✐t❤ ✐ts ✐♠♣❧❡♠❡♥t❛t✐♦♥✱ ❛♥❞ ❦❡❡♣✐♥❣
t❤❡♠ s②♥❝❤r♦♥✐s❡❞ t❤r♦✉❣❤♦✉t t❤❡ ❧✐❢❡t✐♠❡
♦❢ t❤❡ s②st❡♠✳

❬✹❪ ▼❛rt✐♥✲▲ö❢✳ ■♥t✉✐t✐♦♥✐st✐❝
❧✐♦♣♦❧✐s✱ ✶✾✽✹✳

❆♥ ❛❞✈❛♥t❛❣❡ ♦❢ t❤✐s ❛♣✲

♣r♦❛❝❤ ✐s t❤❛t t❤❡ s❦✐❧❧s r❡q✉✐r❡❞ t♦ ❝♦♥str✉❝t

❬✺❪ ◆♦r❡❧❧✳

♣r♦❣r❛♠s ❛r❡ ❞✐r❡❝t❧② ❛♣♣❧✐❝❛❜❧❡ t♦ ✉♥❞❡r✲

❇✐❜✲

❚♦✇❛r❞s ❛ ♣r❛❝t✐❝❛❧ ♣r♦❣r❛♠♠✐♥❣

❧❛♥❣✉❛❣❡ ❜❛s❡❞ ♦♥ ❞❡♣❡♥❞❡♥t t②♣❡ t❤❡♦r②✳

st❛♥❞✐♥❣ t❤❡ s♣❡❝✐✜❝❛t✐♦♥s✳ ❚❤✐s ❛❧s♦ ♠❡❛♥s

P❤❉ t❤❡s✐s✱ ❈❤❛❧♠❡rs✱ ✷✵✵✼✳

t❤❛t t❤❡ ❧✐❜r❛r✐❡s ❜❡❝♦♠❡ s❡❧❢✲❞♦❝✉♠❡♥t✐♥❣✳

❬✻❪ ❈❤❧✐♣❛❧❛ ❡t ❛❧✳ ❊✛❡❝t✐✈❡ ✐♥t❡r❛❝t✐✈❡ ♣r♦♦❢s
❢♦r ❤✐❣❤❡r✲♦r❞❡r ✐♠♣❡r❛t✐✈❡ ♣r♦❣r❛♠s✳ ■♥
■❈❋P ✷✵✵✾✱ ♣✳ ✼✾✳ ❆❈▼✱ ✷✵✵✾✳

❙♦❢t✇❛r❡ ❧✐❜r❛r✐❡s ❤❛✈❡ ❧♦♥❣ ❜❡❡♥ r❡❝♦❣♥✐s❡❞
❛s ✈❡❤✐❝❧❡s ❢♦r ✐♥❝r❡❛s❡❞ s♦❢t✇❛r❡ ♣r♦❞✉❝t✐✈✲
✐t②✳ ❋✐rst✱ t❤❡② ❝❛♣t✉r❡ ❞♦♠❛✐♥ ❦♥♦✇❧❡❞❣❡ ✐♥

❬✼❪ ❉❛♥✐❡❧ss♦♥✳ ❚♦t❛❧ ♣❛rs❡r ❝♦♠❜✐♥❛t♦rs✳ ■♥
■❈❋P ✷✵✶✵✱ ♣✳ ✷✽✺✳ ❆❈▼✱ ✷✵✶✵✳

t❡r♠s ♦❢ s♦❢t✇❛r❡ s♦❧✉t✐♦♥s t♦ t❤❡ ♣r♦❜❧❡♠s
t❤❛t ❛ ✉s❡r ✇❛♥ts t♦ s♦❧✈❡✳ ❙❡❝♦♥❞✱ t❤❡② ❛❞❞

❬✽❪ ❇❡r♥❛r❞② ✫ ❈❧❛❡ss❡♥✳ ❊✣❝✐❡♥t ❞✐✈✐❞❡✲❛♥❞✲
❝♦♥q✉❡r ♣❛rs✐♥❣ ♦❢ ♣r❛❝t✐❝❛❧ ❝♦♥t❡①t✲❢r❡❡
❧❛♥❣✉❛❣❡s✳ ❚♦ ❛♣♣❡❛r ✐♥ ■❈❋P ✷✵✶✸✳

❛ ❧❛②❡r ♦❢ ❛❜str❛❝t✐♦♥ t♦ t❤❡ ✉♥❞❡r❧②✐♥❣ ❝♦♠✲
♣✉t❛t✐♦♥✱ ✇❤✐❝❤ ❛❧❧♦✇s ❞❡✈❡❧♦♣❡rs t♦ ✇r✐t❡
s♦❢t✇❛r❡ ✐♥ t❡r♠s ❝❧♦s❡r t♦ t❤❡✐r ♣r♦❜❧❡♠ ❞♦✲

❬✾❪ ❉❛♥✐❡❧ss♦♥ ✫ ❏❛♥ss♦♥✳ ❈❤❛s✐♥❣ ❜♦tt♦♠s✱ ❛
❝❛s❡ st✉❞② ✐♥ ♣r♦❣r❛♠ ✈❡r✐✜❝❛t✐♦♥✳ ■♥ ▼P❈
✷✵✵✹✱ ▲◆❈❙ ✸✶✷✺✱ ♣✳ ✽✺✳ ❙♣r✐♥❣❡r✳

♠❛✐♥ ❛♥❞ ✉s✉❛❧❧② r❡s✉❧ts ✐♥ ✐♠♣r♦✈❡❞ q✉❛❧✲
✐t② ❛♥❞ r♦❜✉st♥❡ss✳

t②♣❡ t❤❡♦r②✳

❲❡ ❛✐♠ t♦ ❣♦ ❜❡②♦♥❞

st❛t❡✲♦❢✲t❤❡✲❛rt ✇❤❡♥ ✐t ❝♦♠❡s t♦ ❡①♣r❡ss✐✈✲

❬✶✵❪ ◆♦r❡❧❧ ✫ ❏❛♥ss♦♥✳ P♦❧②t②♣✐❝ ♣r♦❣r❛♠♠✐♥❣
✐♥ ❍❛s❦❡❧❧✳ ■♥ ■❋▲ ✷✵✵✸✱ ▲◆❈❙ ✸✶✹✺✱ ♣✳
✶✻✽✳ ❙♣r✐♥❣❡r✱ ✷✵✵✹✳

✐t② ♦❢ ❧✐❜r❛r✐❡s ❢♦r ♣r♦❣r❛♠♠✐♥❣ ✇✐t❤ ❞❡♣❡♥✲
❞❡♥t t②♣❡s✱ ✇❤✐❝❤ ✐s ❛ r❡❧❛t✐✈❡❧② ✉♥❡①♣❧♦r❡❞
♥✐❝❤❡✳ ❇② ❞♦✐♥❣ s♦✱ ✇❡ ❤♦♣❡ t♦ ✐♠♣r♦✈❡ t❤❡

❬✶✶❪ ❏❛♥ss♦♥ ✫ ❏❡✉r✐♥❣✳ ❋✉♥❝t✐♦♥❛❧ ♣❡❛r❧✿ P♦❧②✲
t②♣✐❝ ✉♥✐✜❝❛t✐♦♥✳
❏✳ ❋✉♥❝t✳ Pr♦❣r❛♠✳✱
✽✭✺✮✿✺✷✼✕✺✸✻✱ ✶✾✾✽✳

s♦❢t✇❛r❡ t❡❝❤♥♦❧♦❣② ✜❡❧❞ ✐♥ ❣❡♥❡r❛❧✱ ❛s t❤❡s❡
❧✐❜r❛r✐❡s s❤♦✉❧❞ s❡r✈❡ ❛s ❡①❛♠♣❧❡s ♦❢ ❣♦♦❞
❞❡s✐❣♥ ❢♦r ♦t❤❡r ❛♣♣❧✐❝❛t✐♦♥s✳

❬✶✷❪ ❇❡r♥❛r❞②✳ ▲❛③② ❢✉♥❝t✐♦♥❛❧ ✐♥❝r❡♠❡♥t❛❧
♣❛rs✐♥❣✳ ■♥ ❍❛s❦❡❧❧ ✷✵✵✾✱ ♣✳ ✹✾✳ ❆❈▼✳

❚❤❡ s❝✐❡♥t✐✜❝ ❝♦♥tr✐❜✉t✐♦♥s t♦ t❤❡ ❝♦♠♣✉t❡r
s❝✐❡♥❝❡ ❛r❡❛ ✇✐❧❧ ❜❡ ✐♥ t❤❡ ❢♦r♠ ♦❢ ♦♣❡♥

❬✶✸❪ ❇❡r♥❛r❞② ✫ ▼♦✉❧✐♥✳ ❚②♣❡✲t❤❡♦r② ✐♥ ❝♦❧♦r✳
❚♦ ❛♣♣❡❛r ✐♥ ■❈❋P ✷✵✶✸✳

s♦✉r❝❡ s♦❢t✇❛r❡ ♣r♦t♦t②♣❡s✱ ❞♦❝t♦r❛❧ tr❛✐♥✲
✐♥❣✱ ❝♦♥❢❡r❡♥❝❡ ❛♥❞ ❥♦✉r♥❛❧ ♣❛♣❡rs ❛♥❞ t❛❧❦s

❬✶✹❪ ❇✐r❞ ✫ ❞❡ ▼♦♦r✳ ❆❧❣❡❜r❛ ♦❢ Pr♦❣r❛♠♠✐♥❣✱
✈♦❧✉♠❡ ✶✵✵ ♦❢ ■♥t❡r♥❛t✐♦♥❛❧ ❙❡r✐❡s ✐♥ ❈♦♠✲
♣✉t❡r ❙❝✐❡♥❝❡✳ Pr❡♥t✐❝❡✲❍❛❧❧✱ ✶✾✾✼✳

✭♦♥ t❤❡ t❡❝❤♥✐q✉❡s ✉s❡❞ ❢♦r t❤❡ ❧✐❜r❛r✐❡s ❛s
✇❡❧❧ ❛s ♦♥ t❤❡ ❧❛♥❣✉❛❣❡ ✐♠♣r♦✈❡♠❡♥ts✮✳ ❲❡
❛❧s♦ ❤♦♣❡ t♦ ❤❡❧♣ t❤❡ ✇✐❞❡r r❡s❡❛r❝❤ ❝♦♠♠✉✲

❬✶✺❪ ❲❛❞❧❡r✳ ❚❤❡♦r❡♠s ❢♦r ❢r❡❡✦ ■♥
❋P❈❆ ✶✾✽✾✱ ♣✳ ✸✹✼✳ ❆❈▼✱ ✶✾✽✾✳

♥✐t② ❜② ❝♦♥tr✐❜✉t✐♥❣ str♦♥❣❧② t②♣❡❞ ❧✐❜r❛r✐❡s
❢♦r ✐♥❝r❡❛s✐♥❣❧② ❝♦rr❡❝t s❝✐❡♥t✐✜❝ ❝♦♠♣✉t✐♥❣✳

✺

Pr♦❝✳ ♦❢

Kod

2013-2993-108682-9
Name of applicant

Jansson, Patrik
Date of birth

720311-7515
Title of research programme

Strongly Typed Libraries for Programs and Proofs

Appendix

B

Curriculum vitae

VRAPS/VR-Direct bilaga 2004.Be

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

❆♣♣❡♥❞✐① ❇

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❈✉rr✐❝✉❧✉♠ ❱✐tæ✿ P❛tr✐❦ ❏❛♥ss♦♥✱ ✶✾✼✷✲✵✸✲✶✶
✶✳ ❍✐❣❤❡r ❡❞✉❝❛t✐♦♥ ❞❡❣r❡❡✿
✶✾✾✺✿

❇❙❝✰▼❙❝ ❞❡❣r❡❡s ✐♥ ❊♥❣✐♥❡❡r✐♥❣ P❤②s✐❝s ✰ ❊♥❣✐♥❡❡r✐♥❣ ▼❛t❤❡♠❛t✐❝s ❢r♦♠ ❈❤❛❧♠❡rs✱

❙✇❡❞❡♥✳ ■ ❣r❛❞✉❛t❡❞ ❛❧♠♦st t✇♦ ②❡❛rs ❜❡❢♦r❡ s❝❤❡❞✉❧❡ ❛s t❤❡ ❜❡st st✉❞❡♥t ♦❢ ♠② ②❡❛r✳

✷✳ ❉♦❝t♦r❛❧ ❞❡❣r❡❡✿
✷✵✵✵✿

Pr♦❣r❛♠♠✐♥❣

P❤✳❉✳ ❞❡❣r❡❡ ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ❢r♦♠ ❈❤❛❧♠❡rs✱ ❙✇❡❞❡♥✱ ♦♥
✱ ❆❞✈✐s♦r✿ ❏♦❤❛♥ ❏❡✉r✐♥❣✳

❋✉♥❝t✐♦♥❛❧ P♦❧②t②♣✐❝

✸✳ P♦st❉♦❝ ❛♥❞ ❣✉❡st r❡s❡❛r❝❤✿
✶✾✾✽✱ ✶✾✾✽✱ ✷✵✵✶✿

❘❡s❡❛r❝❤ ✈✐s✐ts ✭✷ ✰ ✷ ✰ ✸ ♠♦♥t❤s✮ t♦ ◆♦rt❤❡❛st❡r♥ ❯♥✐✈❡rs✐t②✱ ❇♦st♦♥✱

❯❙❆❀ ❖①❢♦r❞ ❯♥✐✈❡rs✐t② ❈♦♠♣✉t✐♥❣ ▲❛❜✱ ❯❑❀ ❉❡♣t✳ ♦❢ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡✱ ❨❛❧❡✱ ❯❙❆✳

✷✵✵✵✕✷✵✵✶✿

P♦st❉♦❝✱ ❈❤❛❧♠❡rs✳

✹✳ ◗✉❛❧✐✜❝❛t✐♦♥ ❛s ❆ss♦❝✐❛t❡ Pr♦❢❡ss♦r✿
✷✵✵✹✿

❉♦❝❡♥t ✭❆ss♦❝✐❛t❡ Pr♦❢❡ss♦r✮ ❞❡❣r❡❡ ❢r♦♠ ❈❤❛❧♠❡rs✱ ❙✇❡❞❡♥✳

✺✳ ❈✉rr❡♥t ❊♠♣❧♦②♠❡♥t✿
✷✵✶✶✕♥♦✇✿

Pr♦❢❡ss♦r✱ ❈❤❛❧♠❡rs✳ ❘❡s❡❛r❝❤ ✺✵✪ ✭✷✵✶✸✮✳

✻✳ Pr❡✈✐♦✉s ❊♠♣❧♦②♠❡♥t ❛♥❞ ❊❞✉❝❛t✐♦♥✿
✷✵✵✶✕✷✵✵✹✿
✷✵✵✹✕✷✵✶✶✿

❆ss✐st❛♥t Pr♦❢❡ss♦r ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡✱ ❈❤❛❧♠❡rs✳
❆ss♦❝✐❛t❡ Pr♦❢❡ss♦r✱ ❈❤❛❧♠❡rs✳

✼✳ ❙✉♣❡r✈✐s✐♦♥✱ ❞♦❝t♦r❛t❡s ❛♥❞ ♣♦st❞♦❝s✿
■ ✇❛s P❤❉ ❛❞✈✐s♦r ♦❢ ❯❧❢ ◆♦r❡❧❧ ✭P❤❉ ✷✵✵✼✮✱ ◆✐❧s ❆♥❞❡rs ❉❛♥✐❡❧ss♦♥ ✭P❤❉ ✷✵✵✼✮ ❛♥❞ ❏❡❛♥✲
P❤✐❧✐♣♣❡ ❇❡r♥❛r❞② ✭P❤❉ ✷✵✶✶✮✳ ■ ✇♦r❦❡❞ ♦♥ ❣❡♥❡r✐❝ ♣r♦❣r❛♠s ❛♥❞ ♣r♦♦❢s ✇✐t❤ ◆♦r❡❧❧✱ ♦♥
♣r♦❣r❛♠ ❝♦rr❡❝t♥❡ss t❤r♦✉❣❤ t②♣❡s ✇✐t❤ ❉❛♥✐❡❧ss♦♥ ❛♥❞ ♣❛r❛♠❡tr✐❝✐t② ❢♦r ❞❡♣❡♥❞❡♥t t②♣❡s
✫ t❡st✐♥❣ ✇✐t❤ ❇❡r♥❛r❞②✳ ❆❧❧ t❤r❡❡ ❛r❡ st✐❧❧ ✐♥ ❛❝❛❞❡♠✐❛✳
■ ❤❛✈❡ ❛❧s♦ s✉♣❡r✈✐s❡❞ ❢♦✉r P♦st❉♦❝s✿ ●ré❣♦✐r❡ ❍❛♠♦♥ ❛♥❞ ❆♥❞r❡❛s ❆❜❡❧ ✭✷✵✵✸✕✷✵✵✺✮✱
❏❡❛♥✲P❤✐❧✐♣♣❡ ❇❡r♥❛r❞② ✭✷✵✶✶✕✷✵✶✷✮ ❛♥❞ ♥♦✇ ❈❡③❛r ■♦♥❡s❝✉ ✭✷✵✶✸✕✮✳

✶

❆♣♣❡♥❞✐① ❇

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

■ ❝✉rr❡♥t❧② s✉♣❡r✈✐s❡ t❤❡ P❤❉ st✉❞❡♥t ❏♦♥❛s ❉✉r❡❣år❞ ✭▲✐❝✳ ❉❡❝✳ ✷✵✶✷✮✳ ■ ❛♠ ❛❧s♦ ❡①❛♠✐♥❡r
✭❜✉t ♥♦t s✉♣❡r✈✐s♦r✮ ♦❢ t❤r❡❡ ♦t❤❡r P❤❉ st✉❞❡♥ts✿ ❘❛♠♦♥❛ ❊♥❛❝❤❡✱ ❉❛♥ ❘♦sé♥ ❛♥❞ ❆♥t♦♥
❊❦❜❧❛❞✳
■ ❤❛✈❡ ❜❡❡♥ ❛ ♠❡♠❜❡r ♦❢ t❤❡ ❡✈❛❧✉❛t✐♦♥ ❝♦♠♠✐tt❡❡ ♦❢ t❤r❡❡ P❤❉ ❞❡❢❡♥❝❡s ❛t ❈❤❛❧♠❡rs ✭❚✳
●❡❞❡❧❧✱ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ✭✷✵✵✽✮✱ ▼✳ ❩❛❧❡✇s❦✐✱ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ✭✷✵✵✽✮✱ ❍✳ ❏♦❤❛♥ss♦♥✱
P❤②s✐❝s ✭✷✵✶✵✮✮✳ ■ ❤❛✈❡ ❛❧s♦ s✉♣❡r✈✐s❡❞ ♦✈❡r ✷✵ ▼❙❝ ❛♥❞ ❇❙❝ ♣r♦❥❡❝t st✉❞❡♥ts✳

✽✳ ◆❛t✐♦♥❛❧ ♦r ✐♥t❡r♥❛t✐♦♥❛❧ ❞✐st✐♥❝t✐♦♥s ❛♥❞ ❛✇❛r❞s✿
◆❛t✐♦♥❛❧ ❛♥❞ ✐♥t❡r♥❛t✐♦♥❛❧ ❣r❛♥ts✿
✶✾✾✼✕✷✵✵✹✿
✷✵✵✸✕✷✵✵✺✿

✈❡❧♦♣♠❡♥t

❈♦✲❛♣♣❧✐❝❛♥t ♦♥

❢✉♥❞❡❞ ✇✐t❤

✷✵✵✸✕✷✵✵✺✿
❢✉♥❞❡❞ ✇✐t❤

✷✵✵✾✕✷✵✶✷✿

▲❛♥❣✉❛❣❡s

❖❜t❛✐♥❡❞ tr❛✈❡❧ ❣r❛♥ts ✭

✷✼✼❦ ❙❊❑ ✐♥ t♦t❛❧✮ ❢r♦♠ s❡✈❡r❛❧ ♣r✐✈❛t❡ ❢♦✉♥❞❛t✐♦♥s

❈♦✈❡r ✖ ❈♦♠❜✐♥✐♥❣ ❱❡r✐✜❝❛t✐♦♥ ▼❡t❤♦❞s ✐♥ ❙♦❢t✇❛r❡ ❉❡✲
●❡♥❡r✐❝ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠s ❛♥❞ Pr♦♦❢s
❙♦❢t✇❛r❡ ❉❡s✐❣♥ ❛♥❞ ❱❡r✐✜❝❛t✐♦♥ ✉s✐♥❣ ❉♦♠❛✐♥ ❙♣❡❝✐✜❝

✽▼ ❙❊❑ ❜② t❤❡ ❙✇❡❞✐s❤ ❋♦✉♥❞❛t✐♦♥ ❢♦r ❙tr❛t❡❣✐❝ ❘❡s❡❛r❝❤✳

▼❛✐♥ ❛♣♣❧✐❝❛♥t ♦♥ t❤❡ ♣r♦❥❡❝t

✶✳✽▼ ❙❊❑ ❜② ❱❘✳
❈♦✲❛♣♣❧✐❝❛♥t ♦♥ ✏

✑ ❢✉♥❞❡❞ ✇✐t❤

✶✶▼ ❙❊❑

❜② t❤❡ ❙✇❡❞✐s❤ ❙❝✐❡♥❝❡ ❈♦✉♥❝✐❧ ✭❱❘✱ ♠✉❧t✐✲♣r♦❥❡❝t

❣r❛♥t ✐♥ str❛t❡❣✐❝ ■♥❢♦r♠❛t✐♦♥ ❛♥❞ ❈♦♠♠✉♥✐❝❛t✐♦♥ ❚❡❝❤♥♦❧♦❣②✮✳

✷✵✶✵✕✷✵✶✸✿

❙②st❡♠s ❉②♥❛♠✐❝s ❛♥❞ P♦❧✐❝②

❈♦✲❛♣♣❧✐❝❛♥t ❛♥❞ ✇♦r❦✲♣❛❝❦❛❣❡ ❧❡❛❞❡r ✐♥ t❤❡ ❈♦♦r❞✐♥❛t✐♦♥ ❆❝t✐♦♥ ✏
✑ ✭●❙❉P✮ ❢✉♥❞❡❞ ✇✐t❤

●❧♦❜❛❧

✶✳✸▼ ❊❯❘ ❜② t❤❡ ❊❯ ✭■❈❚✲✷✵✵✾✳✽✳✵

❋✉t✉r❡ ❛♥❞ ❊♠❡r❣✐♥❣ ❚❡❝❤♥♦❧♦❣② ❖♣❡♥ ❝❛❧❧✮✳

❘❆❲ ❋P✿ Pr♦❞✉❝t✐✈✐t② ❛♥❞ P❡r❢♦r♠❛♥❝❡ t❤r♦✉❣❤ ❘❡s♦✉r❝❡
❆✇❛r❡ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣
✷✺▼ ❙❊❑
✷✵✶✶✕✷✵✶✸✿
❙tr♦♥❣❧② ❚②♣❡❞ ▲✐❜r❛r✐❡s ❢♦r Pr♦❣r❛♠s ❛♥❞
Pr♦♦❢s
✷✳✹▼ ❙❊❑
✷✵✶✶✕✷✵✶✻✿

❈♦✲❛♣♣❧✐❝❛♥t ♦♥ ✏

✑ ❢✉♥❞❡❞ ✇✐t❤

❜② t❤❡ ❙✇❡❞✐s❤ ❋♦✉♥❞❛t✐♦♥ ❢♦r

❙tr❛t❡❣✐❝ ❘❡s❡❛r❝❤✳

▼❛✐♥ ❛♣♣❧✐❝❛♥t ♦♥ t❤❡ ♣r♦❥❡❝t

❢✉♥❞❡❞ ✇✐t❤

❜② ❱❘✳

❈♦♠♠✐ss✐♦♥s ♦❢ tr✉st✿
✶✾✾✽✿

❖r❣❛♥✐s❡r ♦❢ t❤❡ ✜rst ❲♦r❦s❤♦♣ ♦♥ ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣ ✭❲●P✮✱ ▼❛rstr❛♥❞✳ ❚❤❡

✇♦r❦s❤♦♣ ❤❛s ❧❛t❡r ❣r♦✇♥ ✐♥t♦ ❛♥ ♦✣❝✐❛❧ ❆ss♦❝✐❛t✐♦♥ ♦❢ ❈♦♠♣✉t✐♥❣ ▼❛❝❤✐♥❡r② ❙♣❡❝✐❛❧
■♥t❡r❡st ●r♦✉♣ ♦♥ Pr♦❣r❛♠♠✐♥❣ ▲❆◆❣✉❛❣❡s ✭❆❈▼ ❙■●P▲❆◆✮ ✇♦r❦s❤♦♣ ❛♥❞ ■✬✈❡ ❜❡❡♥
P❈ ♠❡♠❜❡r ✭✷✵✵✵✮✱ P❈ ❝❤❛✐r ✭✷✵✵✾✮✱ ❙t❡❡r✐♥❣ ❈♦♠♠✐tt❡❡ ♠❡♠❜❡r ✭✷✵✵✾✕✷✵✶✶✮ ❛♥❞ ❈❤❛✐r
♦❢ t❤❡ ❙t❡❡r✐♥❣ ❈♦♠♠✐tt❡❡ ✭✷✵✶✶✕✷✵✶✷✮✳

✷✵✵✶✿ P❈ ♠❡♠❜❡r ♦❢ t❤❡ ❆❈▼ ❙■●P▲❆◆ ❍❛s❦❡❧❧ ❲♦r❦s❤♦♣✳
✷✵✵✽✕♣r❡s❡♥t✿ ❊❧❡❝t❡❞ ♠❡♠❜❡r ♦❢ ■❋■P ✭■♥t❡r♥❛t✐♦♥❛❧ ❋❡❞❡r❛t✐♦♥

❢♦r ■♥❢♦r♠❛t✐♦♥ Pr♦✲

❝❡ss✐♥❣✮ ❲♦r❦✐♥❣ ●r♦✉♣ ✷✳✶ ♦♥ ✏❆❧❣♦r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✑✳

✷✵✵✾✕✷✵✶✶✿ ❊❧❡❝t❡❞ ♠❡♠❜❡r ♦❢ t❤❡ ❢❛❝✉❧t② s❡♥❛t❡✱ ❈❤❛❧♠❡rs✳
✷✵✵✾✕✷✵✶✶✿ ▼❡♠❜❡r ♦❢ t❤❡ ❙t❡❡r✐♥❣ ❣r♦✉♣ ♦❢ ❲♦r❦s❤♦♣ ♦♥ ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣✳
✷✵✵✾✿ P❈ ❈❤❛✐r ❢♦r ❲♦r❦s❤♦♣ ♦♥ ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣
✷

❆♣♣❡♥❞✐① ❇

✷✵✶✶✿

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❖r❣❛♥✐s❡r ♦❢ ❛ ✇♦r❦s❤♦♣ ♦♥ ✏❉♦♠❛✐♥ ❙♣❡❝✐✜❝ ▲❛♥❣✉❛❣❡s ❢♦r ❊❝♦♥♦♠✐❝❛❧ ❛♥❞ ❊♥✈✐✲

r♦♥♠❡♥t❛❧ ▼♦❞❡❧❧✐♥❣✑ ✐♥ ▼❛rstr❛♥❞ ❛s ♣❛rt ♦❢ ❊❯ ❝♦♦r❞✐♥❛t✐♦♥ ❛❝t✐♦♥ ●❙❉P✳

✷✵✶✶✕✷✵✶✷✿
✷✵✶✷✿

❙t❡❡r✐♥❣ ❈♦♠♠✐tt❡❡ ❈❤❛✐r ♦❢ ❲♦r❦s❤♦♣ ♦♥ ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣✳

❲♦r❦s❤♦♣s ❝❤❛✐r ♦❢ t❤❡ ✶✼t❤ ❆❈▼ ❙■●P▲❆◆ ■♥t❡r♥❛t✐♦♥❛❧ ❈♦♥❢❡r❡♥❝❡ ♦♥ ❋✉♥❝✲

t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣ Pr♦❣r❛♠♠✐♥❣ ✭■❈❋P ✷✵✶✷✮✳

✷✵✶✷✿

❖r❣❛♥✐s❡❞ ❛ ✇♦r❦s❤♦♣ ♦♥ ✏❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ♠❡❡ts ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✑ ❛s ♣❛rt

♦❢ t❤❡ ❋✐rst ❖♣❡♥ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡ ✐♥ ❇r✉ss❡❧s✳

✷✵✶✷✿

❈♦✲♦r❣❛♥✐s❡❞ ❛ ✇♦r❦s❤♦♣ ♦♥ ✏▼♦❞❡❧s ❛♥❞ ◆❛rr❛t✐✈❡s ✐♥ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✑ ✇✐t❤

■❧❛♥ ❈❤❛❜❛② ❛s ♣❛rt ♦❢ t❤❡ ❋✐rst ❖♣❡♥ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡ ✐♥ ❇r✉ss❡❧s✳

✷✵✶✸✿

❖r❣❛♥✐s❡❞ t❤❡ ✏●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ✷✵✶✸✿ ▼♦❞❡❧s ❛♥❞ ❉❛t❛✑ ✇♦r❦s❤♦♣ ✐♥ ❇r✉s✲

s❡❧s ✇✐t❤ ▼❛r✐♦ ❘❛s❡tt✐✱ ▼✐❝❤❛❡❧ ❘❡s❝❤ ❛♥❞ ❘❛❧♣❤ ❉✉♠✳

✷✵✶✸✿

❲♦r❦s❤♦♣s ❝❤❛✐r ♦❢ t❤❡ ✶✽t❤ ❆❈▼ ❙■●P▲❆◆ ■♥t❡r♥❛t✐♦♥❛❧ ❈♦♥❢❡r❡♥❝❡ ♦♥ ❋✉♥❝✲

t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣ ✭■❈❋P ✷✵✶✸✮✳

✷✵✶✸✿

❖r❣❛♥✐s❡❞ ❛ ✇♦r❦s❤♦♣ ♦♥ ✧❋♦r♠❛❧ ▲❛♥❣✉❛❣❡s ❛♥❞ ■♥t❡❣r❛t❡❞ Pr♦❜❧❡♠ ❙♦❧✈✐♥❣ ♣r♦✲

❝❡❞✉r❡s ✐♥ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✧✱ ❇r✉ss❡❧s✳

✷✵✶✸✿

❊❞✐t♦r ❢♦r t❤❡ ♦r✐❡♥t❛t✐♦♥ ♣❛♣❡r ✏●❙❙✿ ❚♦✇❛r❞s ❛ ❘❡s❡❛r❝❤ Pr♦❣r❛♠ ❢♦r ●❧♦❜❛❧

❙②st❡♠s ❙❝✐❡♥❝❡✑ ✭✇✐t❤ ❈✳ ❏❛❡❣❡r✱ ❙✳ ✈❛♥ ❞❡r ▲❡❡✉✇✱ ▼✳ ❘❡s❝❤ ❛♥❞ ❏✳ ❉✳ ❚à❜❛r❛✮ ❛s ♣❛rt
♦❢ t❤❡ ❡✛♦rt t♦ ❞❡✜♥❡ ❛ r❡s❡❛r❝❤ ❛r❡❛ ✇✐t❤✐♥ t❤❡ ✉♣❝♦♠✐♥❣ ❊❯ ❢r❛♠❡✇♦r❦ ♣r♦❣r❛♠♠❡
❍♦r✐③♦♥ ✷✵✷✵✳
■ ❤❛✈❡ ❜❡❡♥ r❡✈✐❡✇❡r ❢♦r ❊❯ ❣r❛♥ts ✭✷✵✶✶✱ ✷✵✶✷✮✱ ❏♦✉r♥❛❧ ♦❢ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣✱
❙❝✐❡♥❝❡ ♦❢ ❈♦♠♣✉t❡r Pr♦❣r❛♠♠✐♥❣✱ Pr✐♥❝✐♣❧❡s ♦❢ Pr♦❣r❛♠♠✐♥❣ ▲❛♥❣✉❛❣❡s✱ ■♥t❡r♥❛t✐♦♥❛❧
❈♦♥❢❡r❡♥❝❡ ♦♥ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣✱ ❙②♠♣♦s✐✉♠ ♦♥ ■♠♣❧❡♠❡♥t❛t✐♦♥ ❛♥❞ ❆♣♣❧✐❝❛t✐♦♥
♦❢ ❋✉♥❝t✐♦♥❛❧ ▲❛♥❣✉❛❣❡s ❛♥❞ s❡✈❡r❛❧ ♦t❤❡r ❥♦✉r♥❛❧s ❛♥❞ ❝♦♥❢❡r❡♥❝❡s✳

❆✇❛r❞s ❛♥❞ ♣r✐❝❡s✿
✶✾✾✶✿

❲✐♥♥❡r ♦❢ t❤❡ ❙✇❡❞✐s❤ ◆❛t✐♦♥❛❧ P❤②s✐❝s ❖❧②♠♣✐❛❞

✶✾✾✶✿

❘❡♣r❡s❡♥t❡❞ ❙✇❡❞❡♥ ✐♥ t❤❡ ■♥t❡r♥❛t✐♦♥❛❧ P❤②s✐❝s ❖❧②♠♣✐❛❞s✳

✶✾✾✶✿

❘❡♣r❡s❡♥t❡❞ ❙✇❡❞❡♥ ✐♥ t❤❡ ■♥t❡r♥❛t✐♦♥❛❧ ▼❛t❤❡♠❛t✐❝s ❖❧②♠♣✐❛❞✳

✶✾✾✻✿

❘❡❝❡✐✈❡❞ t❤❡ ❏♦❤♥ ❊r✐❝ss♦♥ ♠❡❞❛❧ ❢♦r ♦✉tst❛♥❞✐♥❣ s❝❤♦❧❛rs❤✐♣✱ ❈❤❛❧♠❡rs

✾✳ ❉❡❞✉❝t✐❜❧❡ t✐♠❡✿
P❛r❡♥t❛❧ ❧❡❛✈❡ ✇✐t❤ ❏✉❧✐❛ ✭✶✾✾✾✮ ❛♥❞ ❊r✐❦ ✭✷✵✵✹✮ ❢♦r ❛ t♦t❛❧ ♦❢ ♦♥❡ ❢✉❧❧ t✐♠❡ ②❡❛r✳

❚❤❡

♣❛rt ♦❢ t❤❡ ❧❡❛✈❡ ✇❤✐❝❤ ✇❛s ❛❢t❡r ♠② P❤❉ ❞❡❣r❡❡ ✭♦♥ ✷✵✵✵✲✵✻✲✶✾✮ ✇❛s ❛ t♦t❛❧ ♦❢ ✷✺✶ ❞❛②s
✭❛r♦✉♥❞ ✽ ♠♦♥t❤s✮ ✇❤✐❝❤ ♠❡❛♥s t❤❡ ❛❞❥✉st❡❞ P❤❉ ❞❛t❡ ✐s

✸

✷✵✵✶✲✵✷✲✷✺✳

❆♣♣❡♥❞✐① ❇

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❘❡❛s♦♥

❙t❛rt ♦❢ ♣❡r✐♦❞ ❊♥❞ ♦❢ ♣❡r✐♦❞ P❡r❝❡♥t❛❣❡ ❚♦t❛❧ ✭❢✉❧❧ t✐♠❡ ❞❛②s✮

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✵✲✵✽✲✵✼

✷✵✵✵✲✵✽✲✶✽

✺✵✪

✶✵✴✷

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✶✲✵✸✲✵✼

✷✵✵✵✲✵✺✲✵✹

✶✵✵✪

✺✽

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✷✲✵✼✲✵✶

✷✵✵✷✲✵✼✲✸✶

✶✵✵✪

✸✶

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✸✲✶✷✲✵✶

✷✵✵✸✲✶✷✲✵✺

✶✵✵✪

✺

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✹✲✵✽✲✶✻

✷✵✵✹✲✵✽✲✷✼

✶✵✵✪

✶✷

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✺✲✵✶✲✷✹

✷✵✵✺✲✵✸✲✷✹

✷✺✪

✻✵✴✹

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✺✲✵✼✲✵✹

✷✵✵✺✲✵✽✲✶✾

✶✵✵✪

✹✼

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✺✲✵✽✲✷✾

✷✵✵✺✲✶✵✲✷✺

✺✵✪

✺✽✴✷

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✺✲✶✶✲✶✹

✷✵✵✻✲✵✹✲✵✼

✷✺✪

✶✷✾✴✹

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✻✲✵✼✲✵✸

✷✵✵✻✲✵✼✲✶✶

✶✵✵✪

✾

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✻✲✵✼✲✶✷

✷✵✵✻✲✵✼✲✶✷

✺✵✪

✶✴✷

P❛r❡♥t❛❧ ❧❡❛✈❡

✷✵✵✻✲✵✽✲✷✶

✷✵✵✻✲✶✵✲✵✹

✷✺✪

✷✼✴✹

❚♦t❛❧

✷✺✶

✶✵✳ ▲❡❛❞❡rs❤✐♣ ❡①♣❡r✐❡♥❝❡✿
✷✵✵✷✕✷✵✵✽✿
✷✵✵✷✕✷✵✵✺✿

▼❡♠❜❡r ♦❢ t❤❡ st❡❡r✐♥❣ ❣r♦✉♣ ♦❢ t❤❡ ❞❡♣❛rt♠❡♥t✳
❉✐r❡❝t♦r ♦❢ ❙t✉❞✐❡s ❢♦r t❤❡ ❇❙❝ ❛♥❞ ▼❙❝ ❡❞✉❝❛t✐♦♥ ❛t t❤❡ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡

❞❡♣❛rt♠❡♥t✳

✷✵✵✺✕✷✵✵✽✿

❱✐❝❡ ❤❡❛❞ ♦❢ t❤❡ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ❛♥❞ ❊♥❣✐♥❡❡r✐♥❣ ❞❡♣t✳

r❡s♣♦♥s✐❜❧❡ ❢♦r

t❤❡ ❇❙❝ ❛♥❞ ▼❙❝ ❡❞✉❝❛t✐♦♥✳

✷✵✵✽✕✷✵✶✵✿

❉❡♣✉t② ♣r♦❥❡❝t ❧❡❛❞❡r ♦❢ t❤❡ ■▼P❆❈❚ ♣r♦❥❡❝t ❛t ❈❤❛❧♠❡rs ✭✏❉❡✈❡❧♦♣♠❡♥t

♦❢ ❈❤❛❧♠❡rs✬ ◆❡✇ ▼❛st❡r✬s Pr♦❣r❛♠♠❡s✑✱

✸✵▼ ❙❊❑✮✳

✷✵✵✾✿ ❍❡❛❞ ♦❢ st❡❡r✐♥❣ ❣r♦✉♣ ♦❢ ❈❤❛❧♠❡rs ❡❙❝✐❡♥❝❡ ■♥✐t✐❛t✐✈❡✳
✷✵✶✶✕✷✵✶✸✿ ❍❡❛❞ ♦❢ t❤❡ ✺✲②❡❛r ❡❞✉❝❛t✐♦♥ ♣r♦❣r❛♠♠❡ ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ❛♥❞ ❊♥❣✐♥❡❡r✲
✐♥❣ ✭❈✐✈✐❧✐♥❣❡♥❥ör ❉❛t❛t❡❦♥✐❦✱ ❈❤❛❧♠❡rs✮✳

✷✵✶✸✕✿

❍❡❛❞ ♦❢ t❤❡ ❉✐✈✐s✐♦♥ ♦❢ ❙♦❢t✇❛r❡ ❚❡❝❤♥♦❧♦❣②✱ ❈❤❛❧♠❡rs ❛♥❞ ❯♥✐✈❡rs✐t② ♦❢ ●♦t❤❡♥✲

❜✉r❣ ✭✸✵✪ ♦❢ ❢✉❧❧ t✐♠❡ ✴ ②❡❛r✮✳ ❆r♦✉♥❞ ✹✵ ❡♠♣❧♦②❡❡s ❛♥❞ ❛ ②❡❛r❧② t✉r♥♦✈❡r ♦❢

✹✼▼ ❙❊❑✳

✶✶✳ ▲❡❝t✉r✐♥❣ ❡①♣❡r✐❡♥❝❡✿
❇❙❝ ❧❡✈❡❧ ❝♦✉rs❡s✿

▲❡❝t✉r❡r ♦♥ ■♠♣❡r❛t✐✈❡ Pr♦❣r❛♠♠✐♥❣ ✐♥ ❆❞❛ ✭✶✾✾✽✱ ✶✾✾✼✮✱ Pr♦✲

❣r❛♠♠✐♥❣ ▲❛♥❣✉❛❣❡s ✭✷✵✵✵✱ ✷✵✵✶✮✱ ❉❛t❛❜❛s❡s ✭✷✵✵✵✱ ✷✵✵✶✮✱ Pr♦❣r❛♠ ❱❡r✐✜❝❛t✐♦♥ ✭✷✵✵✻✮✱
❛♥❞ s✉♣❡r✈✐s♦r ♦❢ ❇❙❝ t❤❡s❡s ✭✷✵✵✸✱ ✷✵✵✾✮✳

▼❙❝ ❧❡✈❡❧ ❝♦✉rs❡s✿

▲❡❝t✉r❡r ♦❢ ❆❞✈❛♥❝❡❞ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣ ✭✷✵✶✵✱ ✷✵✶✶✱ ✷✵✶✷✱

✷✵✶✸✮✱ ❛♥❞ s✉♣❡r✈✐s♦r ♦❢ ▼❙❝ t❤❡s❡s ✭>

P❤❉ ❧❡✈❡❧ ❝♦✉rs❡s✿

20

st✉❞❡♥ts✱ ✷✵✵✶✕✮

▲❡❝t✉r❡r ♦❢ ❋✉♥❝t✐♦♥❛❧ P♦❧②t②♣✐❝ Pr♦❣r❛♠♠✐♥❣ ✭✷✵✵✵✮✱ ❆❧❣❡❜r❛ ♦❢

Pr♦❣r❛♠♠✐♥❣ ✭✷✵✵✹✱ ✷✵✵✽✮✱ ❈❛t❡❣♦r② ❚❤❡♦r② ❛♥❞ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣ ✭✷✵✶✵✱ ✷✵✶✶✮
❛♥❞ s✉♣❡r✈✐s♦r ♦❢ ❢♦✉r P❤❉ st✉❞❡♥ts ✭✷✵✵✹✕✮✳

✹

Kod

þÿ2013-2993-10Z6Z2-9
Name of applicant

Jansson, Patrik
Date of birth

720311-7515
Title of research programme

Strongly Typed Libraries for Programs and Proofs

Appendix C
List of publications

VRAPS/VR-Direct bilaga 2004.Ce

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se

❆♣♣❡♥❞✐① ❈

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❙❡❧❡❝t❡❞ P✉❜❧✐❝❛t✐♦♥s✿ P❛tr✐❦ ❏❛♥ss♦♥

◆♦t❡ t♦ ♥♦♥ ❝♦♠♣✉t❡r s❝✐❡♥t✐sts

❈♦♥❢❡r❡♥❝❡ ❛rt✐❝❧❡s ✐♥ ❝♦♠♣✉t❡r s❝✐❡♥❝❡ ❛r❡ ♣❡❡r

P❖P▲

■❈❋P

r❡✈✐❡✇❡❞ ❢✉❧❧ ❛rt✐❝❧❡s ✖ ♥♦t ✶✕✷ ♣❛❣❡ ❛❜str❛❝ts✱ ❛♥❞ ❛r❡ t❤❡ ♥♦r♠❛❧ ❢♦r♠ ♦❢ r❡❢❡r❡❡❞ ♣✉❜✲
❧✐❝❛t✐♦♥✳ ❚❤❡ t♦♣ ❝♦♥❢❡r❡♥❝❡s ✐♥ ❡❛❝❤ s✉❜✜❡❧❞ ✭❧✐❦❡

❛♥❞

❜❡❧♦✇✮ t②♣✐❝❛❧❧② ❤❛✈❡

t❤❡ ❤✐❣❤❡st ✐♠♣❛❝t ❢❛❝t♦r ✇✐t❤✐♥ t❤❛t ✜❡❧❞✱ ❤✐❣❤❡r ❡✈❡♥ t❤❛♥ ❛♥② ❥♦✉r♥❛❧✳
❚❤❡ ♣✉❜❧✐❝❛t✐♦♥s ♠♦st r❡❧❡✈❛♥t ❢♦r t❤✐s r❡s❡❛r❝❤ ♣r♦❥❡❝t ❛r❡ ♠❛r❦❡❞ ✇✐t❤ ❛♥ ❛rr♦✇ ✭⇒✮✳

✵✳ ▼♦st ❝✐t❡❞ ♣✉❜❧✐❝❛t✐♦♥s ✭●♦♦❣❧❡ ❙❝❤♦❧❛r✱ ✷✵✶✸✲✵✾✲✵✸✮

✶✼✱ ❤✐s t♦t❛❧ ❝✐t❛t✐♦♥ ❝♦✉♥t ✐s ✶✷✼✾ ❛♥❞ t❤❡ ❢♦❧❧♦✇✐♥❣ ♣❛♣❡rs ❛r❡

❏❛♥ss♦♥✬s ❍✐rs❝❤✲✐♥❞❡① ✐s

t❤❡ ✜✈❡ ♠♦st ❝✐t❡❞ ✭♥♦t ✐♥❝❧✉❞✐♥❣ t❤❡ ♣❛♣❡rs ✐♥ t❤❡ ❧❛st ✽ ②❡❛rs✮✳

Pr♦❝✳ P❖P▲✬✾✼✿ Pr✐♥❝✐♣❧❡s ♦❢ Pr♦❣r❛♠♠✐♥❣ ▲❛♥❣✉❛❣❡s

✶✳ P✳ ❏❛♥ss♦♥ ❛♥❞ ❏✳ ❏❡✉r✐♥❣✳ P♦❧②P ✖ ❛ ♣♦❧②t②♣✐❝ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥❣✉❛❣❡ ❡①t❡♥s✐♦♥✳ ■♥
✱ ♣❛❣❡s ✹✼✵✕✹✽✷✳ ❆❈▼ Pr❡ss✱

✶✾✾✼✳ ❞♦✐✿✶✵✳✶✶✹✺✴✷✻✸✻✾✾✳✷✻✸✼✻✸✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✸✶✹✳

❆❞✈❛♥❝❡❞ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣

▲◆❈❙

✷✳ ❘✳ ❇❛❝❦❤♦✉s❡✱ P✳ ❏❛♥ss♦♥✱ ❏✳ ❏❡✉r✐♥❣✱ ❛♥❞ ▲✳ ▼❡❡rt❡♥s✳ ●❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣✿ ❆♥
✐♥tr♦❞✉❝t✐♦♥✳

■♥

✱ ✈♦❧✉♠❡ ✶✻✵✽ ♦❢

✷✽✕✶✶✺✳ ❙♣r✐♥❣❡r✱ ✶✾✾✾✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

❤tt♣✿✴✴✇✇✇✳❝s❡✳❝❤❛❧♠❡rs✳s❡✴⑦♣❛tr✐❦❥✴♣♦❧②✴❛❢♣✾✽✴✳

✶✽✻✳

❆❞✈❛♥❝❡❞ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣ ✬✾✻

✸✳ ❏✳ ❏❡✉r✐♥❣ ❛♥❞ P✳ ❏❛♥ss♦♥✳
❡❞✐t♦rs✱

❙♣r✐♥❣❡r✲❱❡r❧❛❣✱ ✶✾✾✻✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✱ ♣❛❣❡s

P♦❧②t②♣✐❝ ♣r♦❣r❛♠♠✐♥❣✳

▲◆❈❙

■♥ ❏✳ ▲❛✉♥❝❤❜✉r② ❡t ❛❧✳✱

✱ ✈♦❧✉♠❡ ✶✶✷✾ ♦❢

✱ ♣❛❣❡s ✻✽✕✶✶✹✳

❤tt♣✿✴✴✇✇✇✳❝s❡✳❝❤❛❧♠❡rs✳s❡✴⑦♣❛tr✐❦❥✴♣♦❧②✴❆❋P✾✻✳♣❞❢✳

✶✻✵✳

◆♦r❞✐❝ ❏♦✉r♥❛❧ ♦❢ ❈♦♠♣✉t✐♥❣

✹✳ ▼✳ ❇❡♥❦❡✱ P✳ ❉②❜❥❡r✱ ❛♥❞ P✳ ❏❛♥ss♦♥✳ ❯♥✐✈❡rs❡s ❢♦r ❣❡♥❡r✐❝ ♣r♦❣r❛♠s ❛♥❞ ♣r♦♦❢s ✐♥
❞❡♣❡♥❞❡♥t t②♣❡ t❤❡♦r②✳
✶✷✸✻✲✻✵✻✹✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿
✺✳

⇒

✱ ✶✵✭✹✮✿✷✻✺✕✷✽✾✱ ✷✵✵✸✳

■❙❙◆

❤tt♣✿✴✴❞❧✳❛❝♠✳♦r❣✴❝✐t❛t✐♦♥✳❝❢♠❄✐❞❂✾✽✺✽✵✶✳

♣✉t❡r Pr♦❣r❛♠♠✐♥❣

✺✾✳

P✳ ❏❛♥ss♦♥ ❛♥❞ ❏✳ ❏❡✉r✐♥❣✳ P♦❧②t②♣✐❝ ❞❛t❛ ❝♦♥✈❡rs✐♦♥ ♣r♦❣r❛♠s✳

❙❝✐❡♥❝❡ ♦❢ ❈♦♠✲

✱ ✹✸✭✶✮✿✸✺✕✼✺✱ ✷✵✵✷✳ ❞♦✐✿✶✵✳✶✵✶✻✴❙✵✶✻✼✲✻✹✷✸✭✵✶✮✵✵✵✷✵✲❳✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✺✶✳

✶✳ P❡❡r✲r❡✈✐❡✇❡❞ ❥♦✉r♥❛❧ ❛rt✐❝❧❡s ✭❧❛st ✽ ②❡❛rs✱ ❡①❝❧✉❞✐♥❣ t❤❡ ❛❜♦✈❡✮

❏♦✉r♥❛❧ ♦❢ ❋✉♥❝t✐♦♥❛❧ Pr♦❣r❛♠♠✐♥❣

✻✳ ❏✳✲P✳ ❇❡r♥❛r❞②✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ❘✳ P❛t❡rs♦♥✳
❢♦r ❞❡♣❡♥❞❡♥t t②♣❡s✳

❞♦✐✿✶✵✳✶✵✶✼✴❙✵✾✺✻✼✾✻✽✶✷✵✵✵✵✺✻✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✶✷✳

✶

Pr♦♦❢s ❢♦r ❢r❡❡ ✖ ♣❛r❛♠❡tr✐❝✐t②
✱ ✷✷✭✵✷✮✿✶✵✼✕✶✺✷✱ ✷✵✶✷✳

❆♣♣❡♥❞✐① ❈

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❏♦✉r♥❛❧ ♦❢ ❋✉♥❝t✐♦♥❛❧

✼✳ ❏✳✲P✳ ❇❡r♥❛r❞②✱ P✳ ❏❛♥ss♦♥✱ ▼✳ ❩❛❧❡✇s❦✐✱ ❛♥❞ ❙✳ ❙❝❤✉♣♣✳ ●❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣ ✇✐t❤

Pr♦❣r❛♠♠✐♥❣

❈✰✰ ❝♦♥❝❡♣ts ❛♥❞ ❍❛s❦❡❧❧ t②♣❡ ❝❧❛ss❡s ✖ ❛ ❝♦♠♣❛r✐s♦♥✳

✱ ✷✵✭✸✕✹✮✿✷✼✶✕✸✵✷✱ ✷✵✶✵✳ ❞♦✐✿✶✵✳✶✵✶✼✴❙✵✾✺✻✼✾✻✽✶✵✵✵✵✶✻❳✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿
✽✳

⇒

✶✵✳

❏✳ ❋✉♥❝t✳ Pr♦❣r❛♠✳

❙✳✲❈✳ ▼✉✱ ❍✳✲❙✳ ❑♦✱ ❛♥❞ P✳ ❏❛♥ss♦♥✳ ❆❧❣❡❜r❛ ♦❢ ♣r♦❣r❛♠♠✐♥❣ ✐♥ ❆❣❞❛✿ ❞❡♣❡♥✲

❞❡♥t t②♣❡s ❢♦r r❡❧❛t✐♦♥❛❧ ♣r♦❣r❛♠ ❞❡r✐✈❛t✐♦♥✳
❞♦✐✿✶✵✳✶✵✶✼✴❙✵✾✺✻✼✾✻✽✵✾✵✵✼✸✹✺✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✱ ✶✾✿✺✹✺✕✺✼✾✱ ✷✵✵✾✳

✽✳

✷✳ P❡❡r✲r❡✈✐❡✇❡❞ ❝♦♥❢❡r❡♥❝❡ ❝♦♥tr✐❜✉t✐♦♥s ✭❧❛st ✽ ②❡❛rs✮
✾✳

⇒

✷✹t❤ ❙②♠♣♦s✐✉♠
♦♥ ■♠♣❧❡♠❡♥t❛t✐♦♥ ❛♥❞ ❆♣♣❧✐❝❛t✐♦♥ ♦❢ ❋✉♥❝t✐♦♥❛❧ ▲❛♥❣✉❛❣❡s ✭■❋▲ ✷✵✶✷✮
❈✳ ■♦♥❡s❝✉ ❛♥❞ P✳ ❏❛♥ss♦♥✳

❉❡♣❡♥❞❡♥t❧②✲t②♣❡❞ ♣r♦❣r❛♠♠✐♥❣ ✐♥ s❝✐❡♥t✐✜❝ ❝♦♠✲

♣✉t✐♥❣✿ ❊①❛♠♣❧❡s ❢r♦♠ ❡❝♦♥♦♠✐❝ ♠♦❞❡❧❧✐♥❣✳

■♥ ❘✳ ❍✐♥③❡✱ ❡❞✐t♦r✱

✱ ▲◆❈❙✳

❙♣r✐♥❣❡r✲❱❡r❧❛❣✱ ✷✵✶✸✳

❉❚P✐♥❙❝✐❈♦♠♣✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

Pr♦❝✳ ❚❨P❊❙ ✷✵✶✶
✭▲■P■❝s✮

❤tt♣✿✴✴✇✐❦✐✳♣♦rt❛❧✳❝❤❛❧♠❡rs✳s❡✴❝s❡✴♣♠✇✐❦✐✳♣❤♣✴❋P✴

✵✳

▲❡✐❜♥✐③ ■♥t❡r♥❛t✐♦♥❛❧ Pr♦❝❡❡❞✐♥❣s ✐♥ ■♥❢♦r♠❛t✐❝s

✶✵✳ ❈✳ ■♦♥❡s❝✉ ❛♥❞ P✳ ❏❛♥ss♦♥✳ ❚❡st✐♥❣ ✈❡rs✉s ♣r♦✈✐♥❣ ✐♥ ❝❧✐♠❛t❡ ✐♠♣❛❝t r❡s❡❛r❝❤✳ ■♥
✱ ✈♦❧✉♠❡ ✶✾ ♦❢

✱ ♣❛❣❡s ✹✶✕✺✹✱ ❉❛❣st✉❤❧✱ ●❡r♠❛♥②✱ ✷✵✶✸✳ ❙❝❤❧♦ss ❉❛❣st✉❤❧✕▲❡✐❜♥✐③✲❩❡♥tr✉♠

❢✉❡r ■♥❢♦r♠❛t✐❦✳ ❞♦✐✿✶✵✳✹✷✸✵✴▲■P■❝s✳❚❨P❊❙✳✷✵✶✶✳✹✶✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

❍❛s❦❡❧❧✬✶✷

✵✳

✶✶✳ ❏✳ ❉✉r❡❣år❞✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ▼✳ ❲❛♥❣✳ ❋❡❛t✿ ❋✉♥❝t✐♦♥❛❧ ❡♥✉♠❡r❛t✐♦♥ ♦❢ ❛❧❣❡❜r❛✐❝
t②♣❡s✳ ■♥

✱ ♣❛❣❡s ✻✶✕✼✷✳ ❆❈▼✱ ✷✵✶✷✳ ❞♦✐✿✶✵✳✶✶✹✺✴✷✸✻✹✺✵✻✳✷✸✻✹✺✶✺✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✺✳

✶✷✳ ❏✳ ❏❡✉r✐♥❣✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ❈✳ ❆♠❛r❛❧✳ ❚❡st✐♥❣ t②♣❡ ❝❧❛ss ❧❛✇s✳ ■♥
✹✾✕✻✵✳ ❆❈▼✱ ✷✵✶✷✳ ❞♦✐✿✶✵✳✶✶✹✺✴✷✸✻✹✺✵✻✳✷✸✻✹✺✶✹✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✵✳

❆❈▼ ❙②♠♣♦s✐✉♠ ♦♥ ❍❛s❦❡❧❧

✶✸✳ ❏✳ ❉✉r❡❣år❞ ❛♥❞ P✳ ❏❛♥ss♦♥✳ ❊♠❜❡❞❞❡❞ ♣❛rs❡r ❣❡♥❡r❛t♦rs✳ ■♥

❍❛s❦❡❧❧✬✶✷

✱ ♣❛❣❡s

Pr♦❝❡❡❞✐♥❣s ♦❢ t❤❡ ✹t❤

✱ ❍❛s❦❡❧❧ ✬✶✶✱ ♣❛❣❡s ✶✵✼✕✶✶✼✱ ◆❡✇ ❨♦r❦✱ ◆❨✱ ❯❙❆✱ ✷✵✶✶✳

❆❈▼✳ ❞♦✐✿✶✵✳✶✶✹✺✴✷✵✸✹✻✼✺✳✷✵✸✹✻✽✾✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿
✶✹✳

⇒❏✳✲P✳
■♥

✺✳

Pr♦❝✳ ✶✺t❤ ❆❈▼ ❙■●P▲❆◆ ✐♥t❡r♥❛t✐♦♥❛❧ ❝♦♥❢❡r❡♥❝❡ ♦♥ ❋✉♥❝t✐♦♥❛❧ ♣r♦❣r❛♠♠✐♥❣

❇❡r♥❛r❞②✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ❘✳ P❛t❡rs♦♥✳ P❛r❛♠❡tr✐❝✐t② ❛♥❞ ❞❡♣❡♥❞❡♥t t②♣❡s✳
✱

♣❛❣❡s ✸✹✺✕✸✺✻✱ ❇❛❧t✐♠♦r❡✱ ▼❛r②❧❛♥❞✱ ✷✵✶✵✳ ❆❈▼✳ ❞♦✐✿✶✵✳✶✶✹✺✴✶✽✻✸✺✹✸✳✶✽✻✸✺✾✷✳
◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿
✶✺✳

⇒

✷✾✳

❊✉r♦♣❡❛♥ ❙②♠♣♦s✐✉♠ ♦♥ Pr♦❣r❛♠♠✐♥❣

▲❡❝t✉r❡

❏✳✲P✳ ❇❡r♥❛r❞②✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ❑✳ ❈❧❛❡ss❡♥✳ ❚❡st✐♥❣ ♣♦❧②♠♦r♣❤✐❝ ♣r♦♣❡rt✐❡s✳ ■♥

❆✳ ●♦r❞♦♥✱ ❡❞✐t♦r✱

✷

✱ ✈♦❧✉♠❡ ✻✵✶✷ ♦❢

❆♣♣❡♥❞✐① ❈

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

◆♦t❡s ✐♥ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡

✱ ♣❛❣❡s ✶✷✺✕✶✹✹✳ ❙♣r✐♥❣❡r✱ ✷✵✶✵✳ ❞♦✐✿ ✶✵✳✶✵✵✼✴✾✼✽✲✸✲✻✹✷✲

✶✶✾✺✼✲✻❴✽✳

✶✽✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

❍❛s❦❡❧❧✬✵✽

✶✻✳ ❆✳ ❘♦❞r✐❣✉❡③✱ ❏✳ ❏❡✉r✐♥❣✱ P✳ ❏❛♥ss♦♥✱ ❆✳ ●❡r❞❡s✱ ❖✳ ❑✐s❡❧②♦✈✱ ❛♥❞ ❇✳ ❈✳ ❞✳ ❙✳ ❖❧✐✈❡✐r❛✳
❈♦♠♣❛r✐♥❣ ❧✐❜r❛r✐❡s ❢♦r ❣❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣ ✐♥ ❍❛s❦❡❧❧✳ ■♥
✶✷✷✳ ❆❈▼✱ ✷✵✵✽✳ ❞♦✐✿✶✵✳✶✶✹✺✴✶✹✶✶✷✽✻✳✶✹✶✶✸✵✶✳

✱ ♣❛❣❡s ✶✶✶✕

✺✾✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✶✼✳ ❉✳ ▲✐♥❝❦❡✱ P✳ ❏❛♥ss♦♥✱ ▼✳ ❩❛❧❡✇s❦✐✱ ❛♥❞ ❈✳ ■♦♥❡s❝✉✳ ●❡♥❡r✐❝ ❧✐❜r❛r✐❡s ✐♥ ❈✰✰ ✇✐t❤

■❋■P ❲♦r❦✐♥❣ ❈♦♥❢✳ ♦♥ ❉♦♠❛✐♥ ❙♣❡❝✐✜❝ ▲❛♥❣✉❛❣❡s

❝♦♥❝❡♣ts ❢r♦♠ ❤✐❣❤✲❧❡✈❡❧ ❞♦♠❛✐♥ ❞❡s❝r✐♣t✐♦♥s ✐♥ ❍❛s❦❡❧❧✿ ❆ ❉❙▲ ❢♦r ❝♦♠♣✉t❛t✐♦♥❛❧

▲◆❈❙

✈✉❧♥❡r❛❜✐❧✐t② ❛ss❡ss♠❡♥t✳
✈♦❧✉♠❡ ✺✻✺✽✴✷✵✵✾ ♦❢
✺❴✶✷✳

■♥

✱

✱ ♣❛❣❡s ✷✸✻✕✷✻✶✱ ✷✵✵✾✳

❞♦✐✿ ✶✵✳✶✵✵✼✴✾✼✽✲✸✲✻✹✷✲✵✸✵✸✹✲

✺✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

Pr♦❝✳ ❆❈▼ ❙■●P▲❆◆ ❲♦r❦s❤♦♣ ♦♥

✶✽✳ ❏✳✲P✳ ❇❡r♥❛r❞②✱ P✳ ❏❛♥ss♦♥✱ ▼✳ ❩❛❧❡✇s❦✐✱ ❙✳ ❙❝❤✉♣♣✱ ❛♥❞ ❆✳ Pr✐❡s♥✐t③✳ ❆ ❝♦♠♣❛r✐✲

●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣ ✭❲●P✮

s♦♥ ♦❢ ❈✰✰ ❝♦♥❝❡♣ts ❛♥❞ ❍❛s❦❡❧❧ t②♣❡ ❝❧❛ss❡s✳ ■♥

✷✶✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✱ ♣❛❣❡s ✸✼✕✹✽✳ ❆❈▼✱ ✷✵✵✽✳ ❞♦✐✿✶✵✳✶✶✹✺✴✶✹✶✶✸✶✽✳✶✹✶✶✸✷✹✳

▼❛t❤❡♠❛t✐❝s ♦❢ Pr♦❣r❛♠ ❈♦♥str✉❝t✐♦♥

▲◆❈❙

✶✾✳ ❙✳✲❈✳ ▼✉✱ ❍✳✲❙✳ ❑♦✱ ❛♥❞ P✳ ❏❛♥ss♦♥✳ ❆❧❣❡❜r❛ ♦❢ ♣r♦❣r❛♠♠✐♥❣ ✉s✐♥❣ ❞❡♣❡♥❞❡♥t t②♣❡s✳
■♥

✱ ✈♦❧✉♠❡ ✺✶✸✸✴✷✵✵✽ ♦❢

✷✽✸✳ ❙♣r✐♥❣❡r✱ ✷✵✵✽✳ ❞♦✐✿ ✶✵✳✶✵✵✼✴✾✼✽✲✸✲✺✹✵✲✼✵✺✾✹✲✾❴✶✺✳

✱ ♣❛❣❡s ✷✻✽✕

✶✷✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

Pr♦❝❡❡❞✐♥❣s

✷✵✳ P✳ ❏❛♥ss♦♥✱ ❏✳ ❏❡✉r✐♥❣✱ ❛♥❞ st✉❞❡♥ts ♦❢ t❤❡ ❯tr❡❝❤t ❯♥✐✈❡rs✐t② ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣

♦❢ ■❋▲ ✷✵✵✻
❝❧❛ss✳

▲◆❈❙

❚❡st✐♥❣ ♣r♦♣❡rt✐❡s ♦❢ ❣❡♥❡r✐❝ ❢✉♥❝t✐♦♥s✳
✱ ✈♦❧✉♠❡ ✹✹✹✾ ♦❢

✶✵✳✶✵✵✼✴✾✼✽✲✸✲✺✹✵✲✼✹✶✸✵✲✺❴✶✸✳

■♥ ❩✳ ❍♦r✈❛t❤✱ ❡❞✐t♦r✱

✱ ♣❛❣❡s ✷✶✼✕✷✸✹✳ ❙♣r✐♥❣❡r✲❱❡r❧❛❣✱ ✷✵✵✼✳

❞♦✐✿

✹✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

Pr♦❝✳ Pr✐♥❝✐♣❧❡s ♦❢ Pr♦❣r❛♠♠✐♥❣ ▲❛♥❣✉❛❣❡s

✷✶✳ ◆✳ ❆✳ ❉❛♥✐❡❧ss♦♥✱ ❏✳ ❍✉❣❤❡s✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ ❏✳ ●✐❜❜♦♥s✳ ❋❛st ❛♥❞ ❧♦♦s❡ r❡❛s♦♥✐♥❣
✐s ♠♦r❛❧❧② ❝♦rr❡❝t✳

■♥

✱ ♣❛❣❡s ✷✵✻✕✷✶✼✳

❆❈▼ Pr❡ss✱ ✷✵✵✻✳ ❞♦✐✿✶✵✳✶✶✹✺✴✶✶✶✶✵✸✼✳✶✶✶✶✵✺✻✳

✺✶✳

◆✉♠❜❡r ♦❢ ❝✐t❛t✐♦♥s✿

✸✳ ❘❡✈✐❡✇ ❛rt✐❝❧❡s✱ ❜♦♦❦ ❝❤❛♣t❡rs✱ ❜♦♦❦s
✷✷✳ ❈✳ ◆✐❦❧❛ss♦♥✱ P✳ ❏❛♥ss♦♥✱ ❛♥❞ P✳ ▲✉♥❞❣r❡♥✳

◆ät✈❡r❦❡t ■♥❣❡♥❥örs✉t❜✐❧❞♥✐♥❣❛r♥❛

str✉❝t✉r❡ ✇✐t❤ ♠❛st❡r✬s ♣r♦❣r❛♠♠❡s ❛t ❈❤❛❧♠❡rs✳ ■♥
✱ ✷✵✵✽✳

❉❡♥ ✷✿❛ ❯t✈❡❝❦❧✐♥❣s❦♦♥❢❡r❡♥s❡♥ ❢ör ❙✈❡r✐❣❡s

✷✸✳ ❈✳ ◆✐❦❧❛ss♦♥✱ P✳ ▲✉♥❞❣r❡♥✱ ❛♥❞ P✳ ❏❛♥ss♦♥✳

✐♥❣❡♥❥örs✉t❜✐❧❞♥✐♥❣❛r

t❡rs♣r♦❣r❛♠ ✲ st✉❞❡♥ts②♥♣✉♥❦t❡r✳

■♥

❯t✈❡❝❦❧✐♥❣s❦♦♥❢❡r❡♥s❡♥ ✷✵✵✽✱

■▼P❆❈❚ ✲ ❡st❛❜❧✐s❤✐♥❣ t❤❡ ❇♦❧♦❣♥❛

✱ ♣❛❣❡s ✹✾✕✺✷✱ ✷✵✵✾✳

✸

❯t✈är❞❡r✐♥❣ ❛✈ ❈❤❛❧♠❡rs ♥②❛ ♠❛s✲

❆♣♣❡♥❞✐① ❈

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

❲●P✬✵✾✿ Pr♦❝❡❡❞✐♥❣s ♦❢ t❤❡ ✷✵✵✾ ❆❈▼ ❙■●P▲❆◆
✇♦r❦s❤♦♣ ♦♥ ●❡♥❡r✐❝ ♣r♦❣r❛♠♠✐♥❣

✷✹✳ P✳ ❏❛♥ss♦♥ ❛♥❞ ❙✳ ❙❝❤✉♣♣✱ ❡❞✐t♦rs✳

✱ ✷✵✵✾✳ ❆❈▼✳ ■❙❇◆ ✾✼✽✲✶✲✻✵✺✺✽✲✺✶✵✲✾✳

❊✉r♦♣❡❛♥ ❙♦❝✐❡t② ❢♦r ❊♥❣✐♥❡❡r✐♥❣
❊❞✉❝❛t✐♦♥ ✭❙❊❋■✮ ✸✼t❤ ❆♥♥✉❛❧ ❈♦♥❢❡r❡♥❝❡
■▼P❆❈❚ ✖ ❙tr❛t❡❣✐❝ ❉❡✈❡❧♦♣♠❡♥t ♦❢ ❈❤❛❧♠❡rs ▼❛st❡r✬s Pr♦✲
❣r❛♠♠❡s
▲❡❛r♥✲
✐♥❣ ❢r♦♠ ■▼P❆❈❚ ◗✉❛❧✐t② ❆ss✉r❛♥❝❡
❤tt♣✿✴✴♣✉❜❧✐❝❛t✐♦♥s✳

✷✺✳ ❈✳ ◆✐❦❧❛ss♦♥ ❛♥❞ P✳ ❏❛♥ss♦♥✳ P❡❞❛❣♦❣✐❝❛❧ ❞❡✈❡❧♦♣♠❡♥t ♦❢ ♠❛st❡r✬s ♣r♦❣r❛♠♠❡s ❢♦r
t❤❡ ❇♦❧♦❣♥❛ str✉❝t✉r❡ ❛t ❈❤❛❧♠❡rs ✲ ■▼P❆❈❚✳ ■♥
✱ ✷✵✵✾✳

✷✻✳ ❍✳ ❉❛♥✐❡❧ss♦♥✱ ❡❞✐t♦r✳

✱ ❝❤❛♣t❡r ▲❡❛r♥✐♥❣ ❢r♦♠ ■▼P❆❈❚ ✫ ◗✉❛❧✐t② ❆ss✉r❛♥❝❡✱ ♣❛❣❡s ✷✸✕✷✹✱ ✺✾✕✻✷✳

❈❤❛❧♠❡rs✱ ✷✵✶✵✳ ■❙❇◆ ✾✼✽✲✾✶✲✻✸✸✲✻✷✵✷✲✻✳ P❛tr✐❦ ❏❛♥ss♦♥ ✇r♦t❡ t❤❡ ❝❤❛♣t❡rs
❛♥❞

✳ ❆✈❛✐❧❛❜❧❡ ❢r♦♠

❧✐❜✳❝❤❛❧♠❡rs✳s❡✴❝♣❧✴r❡❝♦r❞✴✐♥❞❡①✳①sq❧❄♣✉❜✐❞❂✶✶✺✵✷✶✳

✷✼✳ ❈✳ ❏❛❡❣❡r✱ P✳ ❏❛♥ss♦♥✱ ❙✳ ✈❛♥ ❞❡r ▲❡❡✉✇✱ ▼✳ ❘❡s❝❤✱ ❏✳ ❉✳ ❚❛❜❛r❛✱ ❛♥❞ ❘✳ ❉✉♠✳ ●❙❙
♦r✐❡♥t❛t✐♦♥ ♣❛♣❡r ✕ ❜❛❝❦❣r♦✉♥❞ ♠❛t❡r✐❛❧✳ Pr❡♣❛r❡❞ ❛s ♣❛rt ♦❢ t❤❡ ❡✛♦rt t♦ ❞❡✜♥❡ ❛
r❡s❡❛r❝❤ ❛r❡❛ ✇✐t❤✐♥ t❤❡ ✉♣❝♦♠✐♥❣ ❊❯ ❢r❛♠❡✇♦r❦ ♣r♦❣r❛♠♠❡ ❍♦r✐③♦♥ ✷✵✷✵✳✱ ❏✉♥❡
✷✵✶✸✳
✷✽✳ ❈✳ ❏❛❡❣❡r✱ P✳ ❏❛♥ss♦♥✱ ❙✳ ✈❛♥ ❞❡r ▲❡❡✉✇✱ ▼✳ ❘❡s❝❤✱ ❛♥❞ ❏✳ ❉✳ ❚❛❜❛r❛✳
✇❛r❞s ❛ r❡s❡❛r❝❤ ♣r♦❣r❛♠ ❢♦r ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✳ ❆✈❛✐❧❛❜❧❡ ❢r♦♠

❣❧♦❜❛❧✲s②st❡♠s✲s❝✐❡♥❝❡✳❡✉✴❄♣❂✶✺✶✷✳✱

✷✵✶✸✳

●❙❙✿ ❚♦✲

❤tt♣✿✴✴❜❧♦❣✳

■❙❇◆ ✾✼✽✳✸✳✾✹✳✶✻✻✸✲✶✷✲✶✳

❈♦♥❢❡r✲

❡♥❝❡ ❱❡rs✐♦♥✱ ♣r❡♣❛r❡❞ ❢♦r t❤❡ ❙❡❝♦♥❞ ❖♣❡♥ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡ ❏✉♥❡
✶✵✲✶✷✱ ✷✵✶✸✱ ❇r✉ss❡❧s✳

✹✳ P❛t❡♥ts✱ st❛t❡ ❞❛t❡ ♦❢ r❡❣✐str❛t✐♦♥✳
◆♦♥❡✳

✺✳ ❖♣❡♥ ❛❝❝❡ss ❝♦♠♣✉t❡r ♣r♦❣r❛♠s t❤❛t ②♦✉ ❤❛✈❡ ❞❡✈❡❧♦♣❡❞
■ ❞❡s✐❣♥❡❞ ❛♥❞ ✐♠♣❧❡♠❡♥t❡❞ ❛ ❝♦♠♣✐❧❡r ❢♦r t❤❡ ♣♦❧②t②♣✐❝ ❧❛♥❣✉❛❣❡ P♦❧②P ✭✇❤✐❝❤ ■ ✇❛s ❧❛t❡r
✐♥✈♦❧✈❡❞ ✐♥ r❡t✐r✐♥❣ ✐♥ ❢❛✈♦✉r ♦❢ ✐ts s✉❝❝❡ss♦r❀ ●❡♥❡r✐❝ ❍❛s❦❡❧❧✮✿
✷✾✳ P✳ ❏❛♥ss♦♥ ❛♥❞ ❯✳ ◆♦r❡❧❧✳ ❚❤❡ P♦❧②P ✷ ❝♦♠♣✐❧❡r✳ ❆✈❛✐❧❛❜❧❡ ❢r♦♠

❝❤❛❧♠❡rs✳s❡✴⑦♣❛tr✐❦❥✴♣♦❧②✴✱

❤tt♣✿✴✴✇✇✇✳❝s❡✳

✷✵✵✹✳

■ ❤❛✈❡ ♣❛rt✐❝✐♣❛t❡❞ ✐♥ t❤❡ ❞❡✈❡❧♦♣♠❡♥t ♦❢ t❤❡ ❆❣❞❛ ♣r♦♦❢ ❡♥❣✐♥❡ ✭♠❛✐♥❧② t❤r♦✉❣❤ ♠②
P❤❉ st✉❞❡♥ts ❯❧❢ ◆♦r❡❧❧✱ ◆✐❧s ❆♥❞❡rs ❉❛♥✐❡❧ss♦♥ ❛♥❞ ❏❡❛♥✲P❤✐❧✐♣♣❡ ❇❡r♥❛r❞②✮✳ ❚❤❡ ✜rst
❞❡s❝r✐♣t✐♦♥ ♦❢ ❆❣❞❛ ✇❛s ✐♥ t❤❡ P❤❉ t❤❡s✐s ♦❢ ♠② st✉❞❡♥t ❯❧❢ ◆♦r❡❧❧ ✭✷✵✵✼✮ ❛♥❞ ✐t ❤❛s ❜❡❡♥
❝✐t❡❞

50

t✐♠❡s ✴ ②❡❛r s✐♥❝❡ t❤❡♥✱ ✐♥❞✐❝❛t✐♥❣ ❛ q✉✐❝❦ s♣r❡❛❞ ✐♥ ❛❝❛❞❡♠✐❛✳

✸✵✳ ❯✳ ◆♦r❡❧❧ ❡t ❛❧✳ ❆❣❞❛ ✖ ❛ ❞❡♣❡♥❞❡♥t❧② t②♣❡❞ ♣r♦❣r❛♠♠✐♥❣ ❧❛♥❣✉❛❣❡✳ ■♠♣❧❡♠❡♥t❛t✐♦♥
❛✈❛✐❧❛❜❧❡ ❢r♦♠

❤tt♣✿✴✴✇✐❦✐✳♣♦rt❛❧✳❝❤❛❧♠❡rs✳s❡✴❛❣❞❛✴✱

✷✵✵✽✳

■ ❤❛✈❡ ❞❡✈❡❧♦♣❡❞ ❛ ❧✐❜r❛r② ❢♦r s♣❡❝✐❢②✐♥❣ ❛♥❞ ❝❤❡❝❦✐♥❣ ❛❧❣❡❜r❛✐❝ ❧❛✇s ♦❢ ❍❛s❦❡❧❧ t②♣❡ ❝❧❛ss❡s✳

✹

❆♣♣❡♥❞✐① ❈

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

✸✶✳ P✳ ❏❛♥ss♦♥ ❛♥❞ ❏✳ ❏❡✉r✐♥❣✳

❚❤❡ ❤❛s❦❡❧❧ ♣❛❝❦❛❣❡

❤❛s❦❡❧❧✳♦r❣✴♣❛❝❦❛❣❡✴❈❧❛ss▲❛✇s✱

✷✵✶✷✳

❈❧❛ss▲❛✇s

✳

❤tt♣✿✴✴❤❛❝❦❛❣❡✳

■ ❤❛✈❡ ❛❧s♦ ❝♦♥tr✐❜✉t❡❞ t♦ s❡✈❡r❛❧ ♦t❤❡r ❧✐❜r❛r✐❡s ❛♥❞ t♦♦❧s✿

•

✷✵✵✹✕✿ ❈❤❛s✐♥❣❇♦tt♦♠s✿ ❆ ❧✐❜r❛r② ❢♦r ✇♦r❦✐♥❣ ✇✐t❤ ♣❛rt✐❛❧ ❛♥❞ ✐♥✜♥✐t❡ ✈❛❧✉❡s ✐♥
❍❛s❦❡❧❧✿

•

❤tt♣✿✴✴❤❛❝❦❛❣❡✳❤❛s❦❡❧❧✳♦r❣✴♣❛❝❦❛❣❡✴❈❤❛s✐♥❣❇♦tt♦♠s

✷✵✵✻✿ ❚❤❡ ❇◆❋ ❈♦♥✈❡rt❡r ✖ ❛ t♦♦❧ ❢♦r ❣❡♥❡r❛t✐♥❣ ❛ ❝♦♠♣✐❧❡r s❦❡❧❡t♦♥ ❢r♦♠ ❛ ❧❛❜❡❧❧❡❞
❇◆❋ ❣r❛♠♠❛r✿

•

❤tt♣✿✴✴❜♥❢❝✳❞✐❣✐t❛❧❣r❛♠♠❛rs✳❝♦♠✴

✷✵✶✷✿ t❡st✐♥❣✲❢❡❛t✿ ❛ ❧✐❜r❛r② ❢♦r ❡✣❝✐❡♥t❧② ❡♥✉♠❡r❛t✐♥❣ ❧❛r❣❡ ❛❜str❛❝t s②♥t❛① tr❡❡
t②♣❡s✿

❤tt♣✿✴✴❤❛❝❦❛❣❡✳❤❛s❦❡❧❧✳♦r❣✴♣❛❝❦❛❣❡✴t❡st✐♥❣✲❢❡❛t

✻✳ P♦♣✉❧❛r s❝✐❡♥❝❡ ❛rt✐❝❧❡s✴♣r❡s❡♥t❛t✐♦♥s
✸✷✳ P✳ ❏❛♥ss♦♥ ❛♥❞ ❚✳ ❋ü❧ö♣✳ ❆ s✉st❛✐♥❛❜❧❡ ❡♥❡r❣② ❢✉t✉r❡ t❤r♦✉❣❤ ❡❞✉❝❛t✐♦♥ ❛♥❞ r❡s❡❛r❝❤✳
Pr❡s❡♥t❡❞ ❛t t❤❡ ●✷✵ ❨♦✉t❤ ❋♦r✉♠ ❈♦♥❢❡r❡♥❝❡ ❤❡❧❞ ✐♥ ❙t✳P❡t❡rs❜✉r❣✱ ❘✉ss✐❛✱ ✷✵✶✸✲

❤tt♣✿✴✴✇✐❦✐✳♣♦rt❛❧✳❝❤❛❧♠❡rs✳s❡✴❝s❡✴♣♠✇✐❦✐✳♣❤♣✴❋P✴
❙✉st❛✐♥❛❜❧❡❊♥❡r❣②❋✉t✉r❡✱ ✷✵✶✸✳
✵✹✲✶✼✴✷✶✳ ❆✈❛✐❧❛❜❧❡ ❢r♦♠

■♥✈✐t❡❞ ♣r❡s❡♥t❛t✐♦♥s ✭✷✵✵✻✕✷✵✶✸✮
✷✵✵✻✲✶✷✲✶✷✿

✏❚❡st✐♥❣ ♣r♦♣❡rt✐❡s ♦❢ ❣❡♥❡r✐❝ ❢✉♥❝t✐♦♥s✑ ❛t t❤❡ ❲♦r❦✐♥❣ ●r♦✉♣ ✷✳✶ ♦♥ ❆❧✲

❣♦r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✷ ✐♥ ◆❛♠✉r✱ ❇❡❧❣✐✉♠✳

✷✵✵✼✲✵✾✲✶✷✿

✏ ❈♦♠♣❛r✐♥❣ ▲✐❜r❛r✐❡s ❢♦r ●❡♥❡r✐❝ Pr♦❣r❛♠♠✐♥❣ ✐♥ ❍❛s❦❡❧❧✑ ❛t t❤❡ ❲♦r❦✐♥❣

●r♦✉♣ ✷✳✶ ♦♥ ❆❧❣♦r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✸ ✐♥ ❑②♦t♦✱ ❏❛♣❛♥✳

✷✵✵✼✲✵✾✲✶✷✿

✏❆❣❞❛ t✉t♦r✐❛❧✑ ❛t t❤❡ ❲♦r❦✐♥❣ ●r♦✉♣ ✷✳✶ ♦♥ ❆❧❣♦r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞

❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✸ ✐♥ ❑②♦t♦✱ ❏❛♣❛♥✳

✷✵✵✾✲✵✼✲✵✷

✿ ✏ P❡❞❛❣♦❣✐❝❛❧ ❞❡✈❡❧♦♣♠❡♥t ♦❢ ▼❛st❡r✬s Pr♦❣r❛♠♠❡s ❢♦r t❤❡ ❇♦❧♦❣♥❛ ❙tr✉❝✲

t✉r❡ ❛t ❈❤❛❧♠❡rs ✲ ■▼P❆❈❚✑ ❛t t❤❡ ✷✵✵✾ ❆♥♥✉❛❧ ❝♦♥❢❡r❡♥❝❡ ♦❢ t❤❡ ❊✉r♦♣❡❛♥ ❙♦❝✐❡t② ❢♦r
❊♥❣✐♥❡❡r✐♥❣ ❊❞✉❝❛t✐♦♥ ✭❙❊❋■✮✱ ❘♦tt❡r❞❛♠✱ t❤❡ ◆❡t❤❡r❧❛♥❞s✳

✷✵✶✵✲✵✶✲✷✺✿

✏P❛r❛♠❡tr✐❝✐t② ❛♥❞ ❉❡♣❡♥❞❡♥t ❚②♣❡s✑ ❛t t❤❡ ❲♦r❦✐♥❣ ●r♦✉♣ ✷✳✶ ♦♥ ❆❧❣♦✲

r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✺ ✐♥ ❇r❛❣❛✱ P♦rt✉❣❛❧✳

✷✵✶✵✲✵✾✲✷✵✿

✏ ❙✐♠♣❧❡ P✉r❡ ❚②♣❡ ❙②st❡♠ ❊①❛♠♣❧❡s✑ ❛t t❤❡ ❲♦r❦✐♥❣ ●r♦✉♣ ✷✳✶ ♦♥ ❆❧❣♦✲

r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✻ ✐♥ ❆t❧❛♥t✐❝ ❈✐t②✱ ◆❡✇ ❏❡rs❡②✱ ❯❙❆✳

✺

❆♣♣❡♥❞✐① ❈

✷✵✶✶✲✵✾✲✷✷✿

P✳ ❏❛♥ss♦♥✱ ✼✷✵✸✶✶✕✼✺✶✺✱ ❙tr♦♥❣▲✐❜

✏❊♠❜❡❞❞❡❞ P❛rs❡r ●❡♥❡r❛t♦rs✑ ❛t t❤❡ ✷✵✶✶ ❆❈▼ ❙■●P▲❆◆ ❍❛s❦❡❧❧ ❙②♠✲

♣♦s✐✉♠✱ ❚♦❦②♦✱ ❏❛♣❛♥✳

✷✵✶✷✲✶✵✲✵✾✿

✏ ❋✉♥❝t✐♦♥❛❧ ❊♥✉♠❡r❛t✐♦♥ ♦❢ ❆❧❣❡❜r❛✐❝ ❚②♣❡s✑ ❛t t❤❡ ■❋■P ❲♦r❦✐♥❣ ●r♦✉♣

✷✳✶ ♦♥ ❆❧❣♦r✐t❤♠✐❝ ▲❛♥❣✉❛❣❡s ❛♥❞ ❈❛❧❝✉❧✐✱ ♠❡❡t✐♥❣ ★✻✾ ✐♥ ❖tt❛✇❛✱ ❈❛♥❛❞❛✳

✷✵✶✷✲✶✶✲✵✾✿

✏ ❈♦♠♣✉t❡r ❙❝✐❡♥❝❡ ♠❡❡ts ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✑ ❛t t❤❡ ✶st ❖♣❡♥ ●❧♦❜❛❧

❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡✱ ◆♦✈❡♠❜❡r ✽t❤✕✶✵t❤✱ ✷✵✶✷✱ ❇r✉ss❡❧s✱ ❇❡❧❣✐✉♠✳

✷✵✶✸✲✵✻✲✶✵✿

P❧❡♥❛r② ♣r❡s❡♥t❛t✐♦♥ ♦♥ ✏ ■❈❚ ❢♦r ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✑ ❛t t❤❡ ✷♥❞ ●❧♦❜❛❧

❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡ ✐♥ ❇r✉ss❡❧s✱ ❇❡❧❣✐✉♠✳

✷✵✶✸✲✵✻✲✶✶✿

✏ ■❈❚ ❢♦r ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡✑ ❛t t❤❡ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ▲❛♥❣✉❛❣❡s

✇♦r❦s❤♦♣ ✭♣❛rt ♦❢ t❤❡ ✷♥❞ ●❧♦❜❛❧ ❙②st❡♠s ❙❝✐❡♥❝❡ ❈♦♥❢❡r❡♥❝❡✮ ✐♥ ❇r✉ss❡❧s✱ ❇❡❧❣✐✉♠✳

✻

Kod

Dnr

2013-2993-108682-9

2013 -

Name of applicant

Jansson, Patrik
Date of birth

Reg date

720311-7515

2013-09-10 14:20:53

Project title

Strongly Typed Libraries for Programs and Proofs

NT

Grants for distinguished young researchers 2013

Grants for distinguished young researchers

NT-FYF
2013

Appendix S

* Övrigt generellt
Chalmers tekniska högskola
2014

2015

2016

Signatures

2017

2013-01-01 -- 2019-12-31

Applicant

Head of department at host University

Date

Clarifi cation of signature

Telephone

A signature on the application is required not only from the applicant but also from the authorised representative of the administrating
organisation/institution or equivalent (normally the head of the department or establishment where the research is to be conducted). The
signature confirms that the department can accommodate the proposed research, position or equipment; that the costing in the application is
approved for the department's part, that any proposed experimentation on human or animal subjects has been reported, and that the
applicant has reported any secondary occupations and commercial ties (s)he may have, and nothing inconsistent with good research
practice has thereby emerged. The applicant must have discussed these conditions with the representative of the administrating
organisation/institution or equivalent before the latter approves and signs the application.

NOTE the exceptions!
Please note that a different procedure applies for the following types of grants:
•
Infrastructure- Operation Grants
•
Infrastructure- Grants for Expensive Equipment
•
Infrastructure- Grants for Large Databases
•
Framework Grant SIMSAM
•
International Recruitment
For these types of grants the vice-chancellor, instead of the head of department, must sign Appendix S. Thereby (s)he confirms the
commitments of the administrative organization. The details are specified in the Call for Proposals, published at www.vr.se.

Vetenskapsrådets noteringar
Kod

2013-2993-108682-9

VRAPS/VR-Direct b 2

Vetenskapsrådet, Box 1035, SE-101 38 Stockholm, tel. +46 (0)8 546 44 000, vetenskapsradet@vr.se