Church’s thesis and related axioms in Coq’s type theory

Yannick Forster forster@cs.uni-saarland

This is the Coq mechanisation of the paper "Church’s thesis and related axioms in Coq’s type theory ".

How to compile the code

You need The Coq Proof Assistant, version 8.11.0 and the stdpp library installed

Afterwards, you can type make in the coq directory.