Steven Schäfer
Steven Schäfer
PhD student at the Programming Systems Lab, Saarland University
Verified email at ps.uni-saarland.de - Homepage
Title
Cited by
Cited by
Year
Autosubst: Reasoning with de Bruijn terms and parallel substitutions
S Schäfer, T Tebbi, G Smolka
International Conference on Interactive Theorem Proving, 359-374, 2015
542015
Completeness and decidability of de Bruijn substitution algebra in Coq
S Schäfer, G Smolka, T Tebbi
Proceedings of the 2015 Conference on Certified Programs and Proofs, 67-73, 2015
212015
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions
K Stark, S Schäfer, J Kaiser
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
172019
Binder aware recursion over well-scoped de Bruijn syntax
J Kaiser, S Schäfer, K Stark
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
112018
Call-by-push-value in Coq: operational, equational, and denotational theory
Y Forster, S Schäfer, S Spies, K Stark
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
102019
POPLMark reloaded: Mechanizing proofs by logical relations.
A Abel, G Allais, A Hameer, B Pientka, A Momigliano, S Schäfer, K Stark
J. Funct. Program. 29, e19, 2019
102019
Autosubst 2: Towards reasoning with multi-sorted de Bruijn terms and vector substitutions
J Kaiser, S Schäfer, K Stark
Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory …, 2017
92017
Transfinite constructions in classical type theory
G Smolka, S Schäfer, C Doczkal
International Conference on Interactive Theorem Proving, 391-404, 2015
92015
Engineering formal systems in constructive type theory
S Schäfer
Saarländische Universitäts-und Landesbibliothek, 2019
62019
Embedding higher-order abstract syntax in type theory
S Schäfer, K Stark
TYPES 2018, 1, 2018
32018
Tower induction and up-to techniques for CCS with fixed points
S Schäfer, G Smolka
International Conference on Relational and Algebraic Methods in Computer …, 2017
32017
Autosubst: Automation for de Bruijn substitutions
S Schäfer, T Tebbi, G Smolka
6th Coq Workshop (July 2014), 2014
32014
A Small Basis for Homotopy Type Theory
F Rech, S Schäfer
2017
Axiomatic semantics for compiler verification
S Schäfer, S Schneider, G Smolka
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016
2016
The system can't perform the operation now. Try again later.
Articles 1–14