Senior Software Consultant at MLabs consultancy.
Formerly Postdoc in the Programming, Logic and Semantics research group at the Department of Computer Science, IT University of Copenhagen.
I defended my PhD Thesis at the Department of Computer Science and Engineering at Chalmers University of Technology under the supervision of Andreas Abel in September 2018.
More recent publications are listed at DBLP.
On Induction, Coinduction and Equality in Martin-Löf and Homotopy Type Theory. PhD Thesis, 2018.
Decidability of Conversion for Type Theory in Type Theory (with A. Abel, J. Ohman). PACML, Issue POPL, 2018. doi: 10.1145/3158111.
Normalization by evaluation for sized dependent types (with A. Abel, T. Winterhalter). PACMPL, Issue ICFP, 2017. doi: 10.1145/3110277.
Parametric quantifiers for dependent type theory (with A. Nuyts, D. Devriese). PACMPL, Issue ICFP, 2017. doi: 10.1145/3110276.
Streams for Cubical Type Theory [pdf]. Unpublished note, 2017.
Executable relational specifications of polymorphic type systems using prolog (with K. Ahn). LNCS: FLOPS 2016; Kochi; Japan, 2016. doi: 10.1007/978-3-319-29604-3_8.
Guarded Cubical Type Theory: Path Equality for Guarded Recursion [arxiv] (with L. Birkedal, A. Bizjak, R. Clouston, H. Grathwohl, B. Spitters). 25th EACSL Annual Conference on Computer Science Logic. CSL, 2016. doi: 10.4230/LIPIcs.CSL.2016.23.
Lightweight Higher-Order Rewriting in Haskell (with E. Axelsson). Trends in Functional Programming, 2015. doi: 10.1007/978-3-319-39110-6_1. Received the "John McCarthy Best Article" and the "David Turner Best Student Article" awards.
Functions out of Higher Truncations [arxiv] (with P. Capriotti, N. Kraus). 24th EACSL Annual Conference on Computer Science Logic. CSL, 2015. doi: 10.4230/LIPIcs.CSL.2015.359.
Guarded Recursive Types in Type Theory [pdf]. Licenciate Thesis, Chalmers University of Technology, 2015.
A formalized proof of strong normalization for guarded recursive types (with A. Abel). LNCS: APLAS 2014; Singapore, 2014. doi: 10.1007/978-3-319-12736-1_8.
A categorical perspective on pattern unification [pdf] (with A. Abel). UNIF Workshop, 2014.