Completeness and Decidability of de Bruijn Substitution Algebra in Coq. - Steven Schäfer; Gert Smolka; Tobias Tebbi (CPP, 2015)

Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. - Steven Schäfer; Tobias Tebbi; Gert Smolka (ITP, 2015)

Transfinite Constructions in Classical Type Theory. - Gert Smolka; Steven Schäfer; Christian Doczkal (ITP, 2015)

Axiomatic semantics for compiler verification. - Steven Schäfer; Sigurd Schneider; Gert Smolka (CPP, 2016)

Tower Induction and Up-to Techniques for CCS with Fixed Points. - Steven Schäfer; Gert Smolka (RAMiCS, 2017)

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

Call-by-push-value in coq: operational, equational, and denotational theory. - Yannick Forster 002; Steven Schäfer; Simon Spies; Kathrin Stark (CPP, 2019)

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

POPLMark reloaded: Mechanizing proofs by logical relations. - Andreas Abel 001; Guillaume Allais; Aliya Hameer; Brigitte Pientka; Alberto Momigliano; Steven Schäfer; Kathrin Stark (J. Funct. Program., 2019)

Engineering formal systems in constructive type theory. - Steven Schäfer (2019)