Johannes Borgström

Senior Lecturer/Associate Professor at Department of Information Technology; Division of Computing Science

Telephone:: +46 18 471 31 65
E-mail:: johannes.borgstrom@it.uu.se
Visiting address:: Hus 10, Regementsvägen 10
Postal address:: Box 337
751 05 UPPSALA

Download contact information for Johannes Borgström at Department of Information Technology; Division of Computing Science

CV:: Download CV
ORCID:: 0000-0001-5990-5742

Short presentation

I am an associate professor in computing science at the IT department, and responsible for the Bachelor's programme in computer science. My research is in the fields of programming languages and process calculi, with an emphasis on semantics. I am currently working on probabilistic programming languages for Bayesian modelling and inference, and applications of e-graphs to compiler optimization.

Keywords

Biography

I work in the programming languages research group mainly on projects related to semantics of functional and communicating programming languages (eg Erlang) as well as probabilistic (Bayesian) modelling languages.

My previous work in the concurrency group was on the Applied Process Calculi project, where we developed families of small formal modelling languages, called psi calculi, for different kinds of parallel, distributed and communicating systems. The core research issue was 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 were machine-checked using an interactive theorem prover.

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.

Publications

Selection of publications

Recent publications

All publications

Articles in journal

Chapters in book

Roles, Stacks, Histories: A Triple for Hoare

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

Part of Reflections on the Work of C.A.R. Hoare, p. 71-100, Springer, 2010

Conference papers

Conference proceedings (editor)

Monograph doctoral thesis

Equivalences and Calculi for Formal Verification of Cryptographic Protocols

Borgström, Johannes

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

Reports

Negative premises in applied process calculi

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

2013
- Download full text (pdf) of Negative premises in applied process calculi