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
Legal notice, Privacy policy
