My research, projects and blog
Finally, after a year at Uni Konstanz, I gave my Inaugural Lecture as a new Tenure-track Professor of the Department of Information and Computer Science . If you missed it and would like to see a recording of the presentation, it is available at the link below. Credits: Michele De Marchi Presentation Recording The lecture has been an awesome opportunity to share my enthusiasm for my research…
I will be attending the 50th POPL which this year is in Boston, like the very first POPL. I am an author of two of the accepted papers. I will be presenting the first paper, written with Azalea Raad and Viktor Vafeiadis, which is on a proof technique to prove durable linearizability for advanced fine-grained persistent data structures. ArXiv Pdf POPL 2023 The Path to Durable Linearizability E.…
I will be giving two talks at OOPSLA which this year is in Auckland, New Zealand! The first talk is about my work with Dan Frumin, Bas van den Heuvel and Jorge Perez, on a session typed π-calculus obtained through a correspondence with the Logic of Bunched Implication (the core of Separation Logic). ArXiv Pdf OOPSLA 2022 A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched…
I am very happy to announce that from September 2018 I will be a Marie-Curie Fellow at Imperial College. My project “ Ve rification through S ecurity and P rogress A bstractions” (VeSPA) was awarded a Marie-Curie Individual Fellowship for 2 years. I will be working with Philippa Gardner to explore new ways to effectively prove Progress (aka liveness) and Security (eg. secrecy) of concurrent…
I always liked Magritte, his witty enigmas on frame, the hard fundamental questions he explores with such clarity. I particularly resonate with the questions about language and meaning: these fundamental questions motivate both my interests in Computer Science and in Music. About a year ago, I went with some friends to the Schirn museum in Frankfurt which hosted a temporary exposition entitled…
During my PhD I worked on analysis of concurrent programs, using the π-calculus as a model of concurrent computation. The π-calculus is like the λ-calculus of concurrency: a minimalistic calculus to represent concurrent computation (as opposed to sequential) that is universal (can compute any computable function). Although there is great beauty in its theory, people often find its syntax cryptic…
The Winter semester just ended here in Kaiserslautern and I gave the last lecture of the Concurrency Theory course I taught. We covered Petri nets, WSTS and Process Algebra, exploring their theory with the underlying goal of automatic verification. In the middle of the course, I realised that there were times where the students were slightly disoriented by the change of register when changing…
My name is Emanuele D’Osualdo. I know what you are thinking, and I do not blame you. Actually, let me get this straight from the start: I hereby forgive you, fully and pre-emptively, for misspelling or mispronouncing my name or surname. Yes, my name is long and complicated (although it has been pointed out to me that Polish names can be orders of magnitude more complicated), but in fact I am…
So nice of you to ask! What you are looking at is an example of the systems we study in Concurrency Theory. In short, it is an example of a mathematical formalisation of a simple internet protocol; the aim of our research is to design algorithms that can prove properties of these kinds of models. The simulation on the homepage is running a fixed program modelling a server/client system. The orange…