Hi, I'm Simon Spies.

I am a 1st year PhD student with Derek Dreyer at the Max Planck Institute for Software Systems and Saarland Informatics Campus.

My research interests are in program semantics, formal software verification, type systems, programming language design, type theory, and logic. At the moment, I am working on transfinitely step-indexed semantic models and program logics.

I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge.

You can reach me at last name at mpi-sws.org.

Publications

1. Transfinite Step-Indexing for Termination.

   Simon Spies, Neel Krishnaswami, Derek Dreyer.

   48th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2021, Online.

   PDF Website Talk

2. Undecidability of Higher-Order Unification Formalised in Coq.

   Simon Spies, Yannick Forster.

   9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA.

   PDF Coq Development

3. Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory.

   Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark.

   8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal.

   PDF Coq Development