Verified extraction from the Coq proof assistant to OCaml, synthetic computability, and machine-checked undecidability proofs.

Link collection to pdfs of Inria applications