Equivalence of system f and ź2 in Coq based on context morphism lemmas. - Jonas Kaiser; Tobias Tebbi; Gert Smolka (CPP, 2017)

Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. - Jonas Kaiser; Brigitte Pientka; Gert Smolka (FSCD, 2017)

Binder aware recursion over well-scoped de Bruijn syntax. - Jonas Kaiser; Steven Schäfer; Kathrin Stark (CPP, 2018)

Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. - Kathrin Stark; Steven Schäfer; Jonas Kaiser (CPP, 2019)

Formal verification of the equivalence of system F and the pure type system L2. - Jonas Kaiser (2019)

Adapting Sequential Recommender Models to Content Recommendation in Chat Data using Non-Item Page-Models. - Albin Zehe; Elisabeth Fischer; Jonas Kaiser; Toni Wagner; Andreas Hotho (KaRS@RecSys, 2024)