Undecidability of Higher-Order Unification Formalised in Coq
(pdf)
Simon Spies, Yannick Forster
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA
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