Mechanising Syntax with Binders in Coq
(pdf)
Kathrin Stark
PhD Thesis, Saarland University
Coq à la Carte - A Practical Approach to Modular Syntax with Binders
(pdf)
Yannick Forster, Kathrin Stark
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA
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
Hereditarily Finite Sets in Constructive Type Theory
(pdf)
Gert Smolka, Kathrin Stark
Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-27, 2016