Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 10:00 - 10:30 at Sala XII - Keynote 1 and Research Paper Chair(s): Magnus O. Myreen

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.

Mon 14 Jan

CPP-2019
09:00 - 10:30: CPP 2019 - Keynote 1 and Research Paper at Sala XII
Chair(s): Magnus O. MyreenChalmers University of Technology, Sweden
CPP-201909:00 - 10:00
Talk
Amy FeltyUniversity of Ottawa
DOI
CPP-201910:00 - 10:30
Research paper
Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA
DOI