Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

We formalise the algorithmic undecidability of validity, satisfiability, and provability of first-order formulas following a synthetic approach based on the computation native to Coq’s constructive type theory. Concretely, we consider Tarski and Kripke semantics as well as classical and intuitionistic natural deduction systems and provide compact many-one reductions from the Post correspondence problem (PCP). Moreover, developing a basic framework for synthetic computability theory in Coq, we formalise standard results concerning decidability, enumerability, and reducibility without reference to a concrete model of computation. For instance, we prove the equivalence of (an instance of) Post’s theorem with Markov’s principle and provide a convenient technique for establishing the enumerability of inductive predicates such as the considered proof systems and PCP.

Tue 15 Jan

Displayed time zone: Belfast change

16:00 - 17:30
Research Papers: Formalization of Mathematics and Computer AlgebraCPP at Sala XII
Chair(s): Zhong Shao Yale University
16:00
30m
Research paper
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
CPP
Yannick Forster Saarland University, Dominik Kirst Saarland University, Gert Smolka Saarland University
DOI
16:30
30m
Research paper
Verified Solving and Asymptotics of Linear Recurrences
CPP
Manuel Eberl Technische Universität München
DOI
17:00
30m
Meeting
Business Meeting
CPP
Assia Mahboubi INRIA, Magnus O. Myreen Chalmers University of Technology, Sweden