Fabian Brenner: Bachelor's Thesis

Saarland University Computer Science

Formalising the undecidability of finitary PCF in Coq

Advisors: Yannick Forster and Dominik Kirst


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.



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

  • Legal notice, Privacy policy