| Autosubst: Reasoning with de Bruijn terms and parallel substitutions S Schäfer, T Tebbi, G Smolka Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 85 | 2015 |
| 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 | 53 | 2019 |
| POPLMark reloaded: Mechanizing proofs by logical relations A Abel, G Allais, A Hameer, B Pientka, A Momigliano, S Schäfer, K Stark Journal of Functional Programming 29, e19, 2019 | 40 | 2019 |
| 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 | 31 | 2015 |
| 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 | 20 | 2018 |
| Transfinite constructions in classical type theory G Smolka, S Schäfer, C Doczkal Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing …, 2015 | 13 | 2015 |
| 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 | 12 | 2019 |
| 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 | 9 | 2017 |
| Engineering formal systems in constructive type theory S Schäfer Saarländische Universitäts-und Landesbibliothek, 2019 | 6 | 2019 |
| Axiomatic semantics for compiler verification S Schäfer, S Schneider, G Smolka Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 6 | 2016 |
| Embedding higher-order abstract syntax in type theory S Schäfer, K Stark TYPES 2018, 1, 2018 | 3 | 2018 |
| Tower induction and up-to techniques for CCS with fixed points S Schäfer, G Smolka Relational and Algebraic Methods in Computer Science: 16th International …, 2017 | 3 | 2017 |
| Autosubst: Automation for de Bruijn substitutions S Schäfer, T Tebbi, G Smolka 6th Coq Workshop (July 2014), 2014 | 3 | 2014 |
| A Small Basis for Homotopy Type Theory F Rech, S Schäfer | | 2017 |
Gert SmolkaProfessor of Computer Science, Saarland University, Saarland Informatics CampusVerified email at ps.uni-saarland.de
