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

Displayed time zone: Belfast change

09:00 - 10:30
Keynote 1 and Research PaperCPP at Sala XII
Chair(s): Magnus O. Myreen Chalmers University of Technology, Sweden
A Linear Logical Framework in Hybrid
Amy Felty University of Ottawa
Research paper
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA