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:
- program logics for weak memory models based on operational semantics,
- typed meta- and tactic programming for dependently-typed languages.
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 PACMPL (ICFP), 2018
- Mtac2: typed tactics for backward reasoning in Coq PACMPL (ICFP), 2018
- Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris 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 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 Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings, 2013 Project URL