From e17232feac75f1ab7b8f5bbbcbd08e423d368312 Mon Sep 17 00:00:00 2001
From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk>
Date: Tue, 23 Jan 2018 17:03:33 +0000
Subject: [PATCH] Add new file

---
 2017-05-09-Kloos.md | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 2017-05-09-Kloos.md

diff --git a/2017-05-09-Kloos.md b/2017-05-09-Kloos.md
new file mode 100644
index 0000000..a54882b
--- /dev/null
+++ b/2017-05-09-Kloos.md
@@ -0,0 +1,14 @@
+---
+title: Johannes Kloos, visitor from MPI
+---
+[Johannes Kloos]( https://people.mpi-sws.org/~jkloos/), a fourth-year PhD student at the [Max Planck Institute for Software Systems](https://www.mpi-sws.org/) 
+visited the group this week. 
+
+Johannes gave a talk to the group about his current research, on Reasoning about event-based concurrency with Asynchronous Liquid Separation Types.
+
+The talk abstract: I will present work on a program logic and associated type system for reasoning about asynchronous programs manipulating shared 
+mutable state. The logic and type system guarantee the absence of races and the preservation of user-specified invariants using a combination of two ideas: 
+refinement types and concurrent separation logic. The logic track ownership of shared state across concurrently posted tasks and allow reasoning about 
+ownership transfer between tasks using permissions. The type system integrated the logic with refinement types to reason about the contents of the heap, 
+in presence of asynchronous tasks. I will first demonstrate the type system on examples from OCaml, and afterwards sketch some preliminary 
+work in applying it to JavaScript.
\ No newline at end of file
-- 
GitLab