Publication details
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster, Dominique Larchey-Wendling
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, ACM, January 2019
We formally prove the undecidability of entailment in intuitionistic linear logic in Coq. We reduce the Post correspondence problem (PCP) via binary stack machines and Minsky machines to intuitionistic linear logic. The reductions rely on several technically involved formalisations, amongst them a binary stack machine simulator for PCP, a verified low-level compiler for instruction-based languages and a soundness proof for intuitionistic linear logic with respect to trivial phase semantics. We exploit the computability of all functions definable in constructive type theory and thus do not have to rely on a concrete model of computation, enabling the reduction proofs to focus on correctness properties.
Project website
Download PDF
Show BibTeX
@INPROCEEDINGS{ForsterLarchey-Wendling:2018:Undecidability-ILL,
title = {Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines},
author = {Yannick Forster and Dominique Larchey-Wendling},
year = {2019},
month = {Jan},
publisher = {ACM},
booktitle = {8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019},
address = {New York, NY, USA},
}
Login to edit
Legal notice, Privacy policy
