SÖK ANSTÄLLD

Fyll i ett eller flera av fälten.

SÖK ENHET

Fyll i namn eller del av namn.

Johannes Borgström

Johannes Borgström

Kontaktuppgifter

Institutionen för informationsteknologi, Datalogi

E-post:
johannes.borgstrom[AT-tecken]it.uu.se
Telefon:
018-471 3165
Besöksadress:
Rum ITC 1140 ITC, Lägerhyddsv. 2, hus 1
Postadress:
Box 337
751 05 UPPSALA

Jag arbetar som forskarassistent i gruppen för mobila processalgebror vid institutionen för IT. Jag forskar på både programmeringsspråk och processalgebror. Mitt fokus är på nya funktionaliteter och deras semantik, 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 på psi-kalkyler: en klass av modelleringsspråk för kommunicerande system.

Biografi

Detta stycke finns inte på svenska, därför visas den engelska versionen.

I work in the Applied Process Calculi project where we develop families of small formal modelling languages, called psi calculi, for parallel, distributed and communicating systems. The core research issue is to provide expressive modelling languages that still satisfy certain essential meta-theoretical properties: a natural equivalence on systems must be a congruence and entail certain algebraic laws (e.g. commutativity of variable binders and commutative monoid laws for parallel composition). For absolute certainty, the proofs are machine-checked using an interactive theorem prover.
 
Recently, we have extended the psi calculi framework to wireless broadcast communication, and modelled a wireless routing protocol. We have also identified an orthogonal extension to the syntax and semantics of psi calculi that lets us model higher-order communication. My ongoing work treats refinements of the framework to better handle local computation and heterogenous models with different sorts of data, and development of a modelling tool for psi calculus instances.
 
During my postdoc at Microsoft Research in Cambridge I worked on three modern programming language features: probabilistic observations for Bayesian modelling, transactional memory for safe parallel imperative programming, and dependent types for verification of stateful programs.
 
I did my PhD with Uwe Nestmann at EPFL, on process calculi for cryptographic protocols. My main contribution was the definition of novel program equivalences (environment-sensitive notions of bisimulation) that soundly approximate observational process equivalence, and proofs of correspondences and differences between them, solving several open problems.
 
During my time as a PhD student, I also applied the techniques and formalisms of process calculi to other domains, namely modelling and verification of peer-to-peer distributed hash tables, models for modal security logics and visualization of message exchanges.

 

Kontakta katalogansvarig vid den aktuella organisationen (institution eller motsv.) för att rätta ev. felaktigheter.

Skriv ut
Dela sidan på