About me

A photo of Janno A photo of me!

Hi, I am Jan-Oliver Kaiser Janno, a 4th-year PhD student with Derek Dreyer at the Max Planck Institute or Software Systems and Saarland Informatics Campus. My research covers two areas: program logics and dependent types. More specifically, most of my research has been on two topics:

  1. program logics for weak memory models based on operational semantics,
  2. typed meta- and tactic programming for dependently-typed languages.

As part of my research, I am heavily involved in Mtac, a typed meta-programming and tactic language for the Coq proof assistant.

You can find a list of my publications below or at dblp.


  • Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
    • Jan-Oliver Kaiser
    • Hoang-Hai Dang
    • Derek Dreyer
    • Ori Lahav
    • Viktor Vafeiadis
    ECOOP, 2017
  • Pilsner: a compositionally verified compiler for a higher-order imperative language
    • Georg Neis
    • Chung-Kil Hur
    • Jan-Oliver Kaiser
    • Craig McLaughlin
    • Derek Dreyer
    • Viktor Vafeiadis
    ICFP, 2015
  • A Constructive Theory of Regular Languages in Coq
    • Christian Doczkal
    • Jan-Oliver Kaiser
    • Gert Smolka
    CPP, 2013