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, Lägerhyddsvägen 1
- Postal address:
- Box 337
751 05 UPPSALA
- CV:
- Download CV
- ORCID:
- 0000-0001-5990-5742
More information is available to staff who log in.
Short presentation
I am an associate professor in computing science at the IT department, and responsible for the undergraduate programme in computer science. My research is in the fields of programming languages and process calculi. I am currently working on probabilistic programming languages for Bayesian modelling and inference, and nominal process calculi, in particular the psi-calculus framework.
Keywords
- concurrency theory
- operational semantics
- probabilistic programming
- process calculi
- program equivalences
- programming languages
- semantics
Biography
I work
in the concurrency group on 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.
Publications
Selection of publications
- Deriving Probability Density Functions from Probabilistic Functional Programs (2017)
- A Lambda-Calculus Foundation for Universal Probabilistic Programming (2016)
- A Sorted Semantic Framework for Applied Process Calculi (2016)
- Modal Logics for Nominal Transition Systems (2015)
- Tabular (2014)
- Higher-order psi-calculi (2014)
Recent publications
- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages (2021)
- Modal Logics for Nominal Transition Systems (2021)
- Universal probabilistic programming offers a powerful approach to statistical phylogenetics (2021)
- Deriving Probability Density Functions from Probabilistic Functional Programs (2017)
- Weak Nominal Modal Logic (2017)
All publications
Articles
- Modal Logics for Nominal Transition Systems (2021)
- Universal probabilistic programming offers a powerful approach to statistical phylogenetics (2021)
- Deriving Probability Density Functions from Probabilistic Functional Programs (2017)
- A Lambda-Calculus Foundation for Universal Probabilistic Programming (2016)
- A Sorted Semantic Framework for Applied Process Calculi (2016)
- Modal Logics for Nominal Transition Systems (2016)
- The Psi-Calculi Workbench (2015)
- Broadcast psi-calculi with an application to wireless protocols (2015)
- Higher-order psi-calculi (2014)
- Measure transformer semantics for Bayesian machine learning (2013)
- Roles, stacks, histories: A triple for Hoare (2011)
- A Complete Symbolic Bisimilarity for an Extended Spi Calculus (2009)
- A Chart Semantics for the Pi-Calculus (2008)
- Static Equivalence is Harder than Knowledge (2006)
- On bisimulations for the spi calculus (2005)
Books
- Proc. Combined 21st International Workshop on Expressiveness in Concurrency (EXPRESS 2014) and 11th Workshop on Structural Operational Semantics (SOS 2014) (2014)
- Proceedings Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics (2013)
- Equivalences and Calculi for Formal Verification of Cryptographic Protocols (2008)
Conferences
- Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages (2021)
- Weak Nominal Modal Logic (2017)
- Fabular (2016)
- Probabilistic programs as spreadsheet queries (2015)
- Modal Logics for Nominal Transition Systems (2015)
- A Sorted Semantic Framework for Applied Process Calculi (extended abstract) (2014)
- Tabular (2014)
- Deriving Probability Density Functions from Probabilistic Functional Programs (2013)
- A Parametric Tool for Applied Process Calculi (2013)
- Bayesian Inference Using Data Flow Analysis (2013)
- A Model-Learner Pattern for Bayesian Reasoning (2013)
- Maintaining Database Integrity with Refinement Types (2011)
- Verified Stateful Programs with Substructural State and Hoare Types (2011)
- Measure Transformer Semantics for Bayesian Machine Learning (2011)
- Broadcast Psi-calculi with an Application to Wireless Protocols (2011)
- A Compositional Theory for STM Haskell (2009)
- Towards the Application of Process Calculi in the Domain of Peer-to-Peer Algorithms (2008)
- Timed calculus of cryptographic communication (2007)
- Calculus of Cryptographic Communication (2006)
- Verifying a Structured Peer-to-Peer Overlay Network (2005)
- Symbolic Bisimulation in the Spi Calculus (2004)