Search 

Jesper Bengtson
PhD Student

Address: Division of Computer Systems Department of Information Technology Uppsala University Box 337 SE-751 05 Uppsala Sweden Visit: ITC building 1, floor 1, room 1140 Phone: +46 18 - 471 1030 Fax: +46 18 511925 Email: Jesper.Bengtson@it.uu.se

Research

My research focuses on process calculi and theorem proving. I am currently working with the mobility group on creating a generic environment for reasoning about process calculi in the interactive theorem prover Isabelle. To this end, I have modelled the pi-calculus in Isabelle using nominal logic. The proofs I have done so far are that strong equivalence is a congruence as well as all the structural congruence rules for strong bisimulation and strong equivalence. The Isabelle sources can be found here.

Hot off the presses

Weak equivalences in psi-calculi Submitted 2010
Psi-calculi: A framework for mobile processes with nominal data and logic Submitted 2009

I have formalised the results of both of these papers in the interactive theorem prover Isabelle. The sources can be found here. These theories have been developed using Mercurial version 96d053e00ec0 from the Isabelle repository. We are currently working on a version compatible with the latest release, in order to submit to the Isabelle Archive of Formal Proofs.

Publications

Formalising the π-calculus using nominal logic. Jesper Bengtson and Joachim Parrow. In Logical Methods in Computer Science, volume 5, number 2:16, pp 1-36, 2009.

Psi-calculi: Mobile processes, nominal data, and logic. Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. In Proc. 24th Symposium on Logic In Computer Science, pp 39-48, IEEE, 2009.

Psi-calculi in Isabelle. Jesper Bengtson and Joachim Parrow. In Theorem Proving in Higher Order Logics, pp 99-114, volume 5674 of Lecture Notes in Computer Science, Springer-Verlag, 2009.

Extended pi-Calculi. Magnus Johansson, Joachim Parrow, Björn Victor, and Jesper Bengtson. In Automata, Languages and Programming, pp 87-98, volume 5126 of Lecture Notes in Computer Science, Springer-Verlag, 2008.

Refinement Types for Secure Implementations. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. In Proc. 21st IEEE Computer Security Foundations Symposium, pp 17-32, IEEE, 2008.

A completeness proof for bisimulation in the pi-calculus using Isabelle. Jesper Bengtson and Joachim Parrow. In Electronic Notes in Theoretical Computer Science, volume 192, number 1, pp 61-75, 2007.

Formalising the pi-calculus using nominal logic. Jesper Bengtson and Joachim Parrow. In Proceedings of FOSSACS 2007, pp 63-77, 2007.

Web Services as a New Approach to Distributing and Coordinating Semantics-Based Verification Toolkits. Michael Baldamus, Jesper Bengtson, GianLuigi Ferrari, and Roberto Raggi. In Electronic Notes in Theoretical Computer Science, volume 105, pp 11-20, 2004.