Programming Systems Lab: Publications by Yannick Forster

Saarland University Computer Science

Select author:

2019

A certifying extraction with time bounds from Coq to call-by-value λ-calculus   (pdf)
Yannick Forster, Fabian Kunze
Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA

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
4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany

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