Jesper Bengtson

30 papers A* 2A 4B 5Journal 14Unranked 5
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Sound and Complete Projection for Global Types.
J. Autom. Reason.
Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone
2025 J jnl
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction (Artifact).
Dagstuhl Artifacts Ser.
Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone
2025 A conf
Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction.
ECOOP
Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone
2023 B conf
A Sound and Complete Projection for Global Types.
ITP
Dawit Legesse Tirore, Jesper Bengtson, Marco Carbone
2022 J jnl
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.
Log. Methods Comput. Sci.
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2021 B conf
Machine-checked semantic session typing.
CPP
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson
2020 J jnl
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.
CoRR
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2020 J jnl
Actris: session-type based reasoning in separation logic.
Proc. ACM Program. Lang.
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2018 J jnl
Coqoon - An IDE for interactive proof development in Coq.
Int. J. Softw. Tools Technol. Transf.
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
2018 J jnl
Formally verifying exceptions for low-level code with separation logic.
J. Log. Algebraic Methods Program.
Marco Paviotti, Jesper Bengtson
2016 A conf
Coqoon - An IDE for Interactive Proof Development in Coq.
TACAS
Alexander John Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink
2016 A conf
Extensible and Efficient Automation Through Reflective Tactics.
ESOP
Gregory Malecha, Jesper Bengtson
2016 J jnl
Psi-Calculi in Isabelle.
J. Autom. Reason.
Jesper Bengtson, Joachim Parrow, Tjark Weber
2014 — conf
Session Types Meet Separation Logic.
LFMTP
Jesper Bengtson
2012 J jnl
CCS in nominal logic.
Arch. Formal Proofs
Jesper Bengtson
2012 B conf
Charge! - A Framework for Higher-Order Separation Logic in Coq.
ITP
Jesper Bengtson, Jonas Braband Jensen, Lars Birkedal
2012 J jnl
Psi-calculi in Isabelle.
Arch. Formal Proofs
Jesper Bengtson
2012 J jnl
The pi-calculus in nominal logic.
Arch. Formal Proofs
Jesper Bengtson
2011 J jnl
Psi-calculi: a framework for mobile processes with nominal data and logic
Log. Methods Comput. Sci.
Jesper Bengtson, Magnus Johansson, Joachim Parrow, Björn Victor
2011 J jnl
Refinement types for secure implementations.
ACM Trans. Program. Lang. Syst.
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2011 B conf
Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq.
ITP
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski, Lars Birkedal
2010 A* conf
Weak Equivalences in Psi-Calculi.
LICS
Magnus Johansson, Jesper Bengtson, Joachim Parrow, Björn Victor
2009 J jnl
Formalising the pi-calculus using nominal logic
Log. Methods Comput. Sci.
Jesper Bengtson, Joachim Parrow
2009 — conf
Psi-calculi in Isabelle.
TPHOLs
Jesper Bengtson, Joachim Parrow
2009 A* conf
Psi-calculi: Mobile Processes, Nominal Data, and Logic.
LICS
Jesper Bengtson, Magnus Johansson, Joachim Parrow, Björn Victor
2008 — conf
Extended pi-Calculi.
ICALP (2)
Magnus Johansson, Joachim Parrow, Björn Victor, Jesper Bengtson
2008 A conf
Refinement Types for Secure Implementations.
CSF
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2007 — conf
A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle.
SOS@LICS/ICALP
Jesper Bengtson, Joachim Parrow
2007 B conf
Formalising the
FoSSaCS
Jesper Bengtson, Joachim Parrow
2004 — conf
Web Services as a New Approach to Distributing and Coordinating Semantics-Based Veri cation Toolkits.
WSFM
Michael Baldamus, Jesper Bengtson, Gian-Luigi Ferrari, Roberto Raggi