Steven Schäfer - Publications

Journal, conference and workshop publications

Binder Aware Recursion over Well-Scoped de Bruijn Syntax   (pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018, 2018. (To appear)

Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions   (pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
LFMTP, 2017.

Axiomatic Semantics for Compiler Verification   (pdf)
Steven Schäfer, Sigurd Schneider, Gert Smolka
5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, FL, USA, January 20-22, 2016.

Transfinite Constructions in Classical Type Theory   (pdf)
Gert Smolka, Steven Schäfer, Christian Doczkal
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, 2015.

Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions   (pdf)
Steven Schäfer, Tobias Tebbi, Gert Smolka
Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, 2015.

Completeness and Decidability of de Bruijn Substitution Algebra in Coq   (pdf)
Steven Schäfer, Gert Smolka, Tobias Tebbi
Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, 2015.