Johannes Borgström

Universitetslektor vid Institutionen för informationsteknologi; Datalogi

Telefon:: 018-471 31 65
E-post:: johannes.borgstrom@it.uu.se
Besöksadress:: Hus 10, Regementsvägen 10
Postadress:: Box 337
751 05 UPPSALA

Ladda ned kontaktuppgifter för Johannes Borgström vid Institutionen för informationsteknologi; Datalogi

Akademiska meriter:: Docent
CV:: Ladda ned CV
ORCID:: 0000-0001-5990-5742

Kort presentation

Jag är lektor i datavetenskap på avdelningen för datalogi vid institutionen för IT, och programansvarig för kandidatprogrammet i datavetenskap. Min forskning rör semantik för programmeringsspråk och processalgebror, med inriktning mot både tillämpningar och algebraiska egenskaper. Just nu arbetar jag på probabilistiska programmeringsspråk för statistiska modeller och Bayesisk inferens, samt hur e-grafer kan användas för att förbättra optimerande kompilatorer.

Nyckelord

Biografi

Jag arbetar i forskargruppen för programmeringsspråk, huvudsakligen med projekt relaterade till semantik för funktionella och kommunicerande programmeringsspråk (t.ex. Erlang) samt probabilistiska (Bayesianska) modelleringsspråk.

Mitt tidigare arbete var inom projektet Applied Process Calculi, där vi utvecklade familjer av små formella modelleringsspråk, kallade psi-kalkyler, för olika typer av parallella, distribuerade och kommunicerande system. Den centrala forskningsfrågan var att tillhandahålla uttrycksfulla modelleringsspråk som fortfarande uppfyller vissa väsentliga metateoretiska egenskaper: en naturlig ekvivalens mellan system måste vara en kongruens och validera vissa algebraiska lagar (t.ex. kommutativitet för variabelbindare och kommutativa monoidlagar för parallell komposition). För absolut säkerhet kontrollerades bevisen maskinellt med hjälp av en interaktiv teorembevisare.

Under min postdoc vid Microsoft Research i Cambridge arbetade jag med tre slags moderna primitiver i programmeringsspråk: probabilistiska observationer för Bayesiansk modellering, transaktionellt minne för säker parallell imperativ programmering och beroende typer för verifiering av tillståndsberoende program.

Jag doktorerade med Uwe Nestmann vid EPFL på processkalkyler för kryptografiska protokoll. Mitt främsta bidrag var definitionen av nya programekvivalenser (kontextkänsliga bisimuleringar) som på ett korrekt sätt approximerar observationell processekvivalens, samt bevis för korrespondens och skillnader mellan dem vilket löste flera öppna problem.

Under min tid som doktorand tillämpade jag också processkalkylstekniker inom andra områden, nämligen modellering och verifiering av peer-to-peer distribuerade hashtabeller, modeller för modala säkerhetslogiker och visualisering av meddelandeutbyten.

Publikationer

Urval av publikationer

Senaste publikationer

Alla publikationer

Artiklar i tidskrift

Doktorsavhandlingar, monografi

Equivalences and Calculi for Formal Verification of Cryptographic Protocols

Borgström, Johannes

2008
- DOI för Equivalences and Calculi for Formal Verification of Cryptographic Protocols

Kapitel i böcker, delar av antologi

Roles, Stacks, Histories: A Triple for Hoare

Borgström, Johannes; Gordon, Andrew D; Pucella, Riccardo

Ingår i Reflections on the Work of C.A.R. Hoare, s. 71-100, Springer, 2010

Konferensbidrag

Proceedings (redaktörskap)

Rapporter

Negative premises in applied process calculi

Åman Pohjola, Johannes; Borgström, Johannes; Parrow, Joachim; Raabjerg, Palle et al.

2013
- Ladda ner fulltext (pdf) av Negative premises in applied process calculi