Programming Systems Lab: Publications by Yannick Forster

Saarland University Computer Science

Select author:

2019

The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space   (pdf)
Yannick Forster, Fabian Kunze, Marc Roth
Technical Report, Full version appeared as arXiv:1902.07515 (To appear)

Hilbert's Tenth Problem in Coq   (pdf)
Dominique Larchey-Wendling, Yannick Forster
Technical Report (To appear)

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

On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem   (pdf)
Yannick Forster, Dominik Kirst, Gert Smolka
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019

Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines   (pdf)
Yannick Forster, Dominique Larchey-Wendling
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019

2018

Call-by-Value Lambda Calculus as a Model of Computation in Coq   (pdf)
Yannick Forster, Gert Smolka
Journal of Automated Reasoning

Formal Small-step Verification of a Call-by-value Lambda Calculus Machine   (pdf)
Fabian Kunze, Gert Smolka, Yannick Forster
16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6

Verification of PCP-Related Computational Reductions in Coq   (pdf)
Yannick Forster, Edith Heiter, Gert Smolka
Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018

2017

On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control   (pdf)
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
International Conference on Functional Programming, ICFP 2017, Oxford, United Kingdom, September 3-9, 2017

Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq   (pdf)
Yannick Forster, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017


Login to edit


Legal notice, Privacy policy