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

CPP-2019
16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Zhong ShaoYale University
CPP-201916:00 - 16:30
Research paper
Yannick ForsterSaarland University, Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
CPP-201916:30 - 17:00
Research paper
Manuel EberlTechnische Universität München
DOI
CPP-201917:00 - 17:30
Meeting
Assia MahboubiINRIA, Magnus O. MyreenChalmers University of Technology, Sweden