About me

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:

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.

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 Charguéraud
- Derek Dreyer
PACMPL (ICFP), 2018
Mtac2: typed tactics for backward reasoning in Coq
- Jan-Oliver Kaiser
- Beta Ziliani
- Robbert Krebbers
- Yann Ré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