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.

Articles

The articles below are my attempts at communicating my research, and  — eventually, I hope — other thoughts.

Publications

  • MoSeL: a general, extensible modal framework for interactive proofs in separation logic
    • Robbert Krebbers
    • Jacques-Henri Jourdan
    • Ralf Jung
    • Joseph Tassarotti
    • Jan-Oliver Kaiser
    • Amin Timany
    • Arthur Charguéraud
    • Derek Dreyer
    PACMPL (ICFP), 2018
  • Mtac2: typed tactics for backward reasoning in Coq
    • Jan-Oliver Kaiser
    • Beta Ziliani
    • Robbert Krebbers
    • Yann Régis-Gianas
    • Derek Dreyer
    PACMPL (ICFP), 2018
  • Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris
    • Jan-Oliver Kaiser
    • Hoang-Hai Dang
    • Derek Dreyer
    • Ori Lahav
    • Viktor Vafeiadis
    31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain, 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
    Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, 2015 Project URL
  • A Constructive Theory of Regular Languages in Coq
    • Christian Doczkal
    • Jan-Oliver Kaiser
    • Gert Smolka
    Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, 2013 Project URL