Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
(pdf)
Kathrin Stark, Steven Schäfer, Jonas Kaiser
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019.
Call-By-Push-Value in Coq: Operational, Equational and Denotational Theory
(pdf)
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019.
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.
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.
Engineering Formal Systems in Constructive Type Theory
(pdf)
Steven Schäfer
PhD Thesis, Saarland University, 2019.