# Fabian Brenner: Bachelor's Thesis

# Formalising the undecidability of finitary PCF in Coq

**Advisors:** Yannick Forster and Dominik Kirst

## Summary

In 2000, Loader proved that the contextual equivalence for a certain variant of simply-typed lambda calculus called PCF2 is undecidable, providing a negative answer to a long-standing open question regarding denotational semantics of Scott and Plotkin's Programming Computable Functions (PCF). We aim at formalising a synthetic version of Loader's proof, which is well-known to be long and full of technical arguments. In this talk, we introduce PCF2 and relate Loader's result to the formerly long-standing open question. We also discuss why related problems are decidable and why these techniques are not applicable to PCF2.
## References

## Resources

First seminar talk: The undecidability of finitary PCF in Coq
Second seminar talk: The undecidability of PCF2 in synthetic computability

Legal notice, Privacy policy