Engineering Formal Systems in Constructive Type Theory
(pdf)
Steven Schäfer
PhD Thesis, Saarland University
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
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
Embedding Higher-Order Abstract Syntax in Type Theory
(pdf)
Steven Schäfer, Kathrin Stark
24th International Conference on Types for Proofs and Programs, TYPES 2018, Braga, Portugal, June 18 - 21
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
Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
(pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
LFMTP
Tower Induction and Up-To Techniques for CCS with Fixed Points
(pdf)
Steven Schäfer, Gert Smolka
Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings
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
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
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
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