Programming Systems Lab: Publications by Steven Schäfer

Saarland University Computer Science

Select author:

2019

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

2018

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

2017

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

2016

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

2015

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


Login to edit


Legal notice, Privacy policy