Write a Blog >>
Tue 21 Jan 2020 16:18 - 16:40 at Maurepas - Formalized mathematics 1 Chair(s): Robert Y. Lewis

The labeled multigraphs of treewidth at most two can be described using a simple term language over which isomorphism of the denoted graphs can be finitely axiomatized. We formally verify soundness and completeness of such an axiomatization using Coq and the mathematical components library. The completeness proof is based on a normalizing and confluent rewrite system on term-labeled graphs. While for most of the development a dependently typed representation of graphs based on finite types of vertices and edges is most convenient, we switch to a graph representation employing a fixed type of vertices shared among all graphs for establishing confluence of the rewrite system. The completeness result is then obtained by transferring confluence from the fixed-type setting to the dependently typed setting.

Tue 21 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: CPP 2020 - Formalized mathematics 1 at Maurepas
Chair(s): Robert Y. LewisVrije Universiteit Amsterdam
CPP-2020-papers15:35 - 15:56
Patrick MassotUniversité Paris Sud, Kevin BuzzardImperial College London, Johan CommelinUniversität Freiburg
DOI Pre-print Media Attached File Attached
CPP-2020-papers15:56 - 16:18
Abhishek Kr SinghTata Institute of Fundamental Research Mumbai, Raja NatarajanTata Institute of Fundamental Research Mumbai
DOI Pre-print Media Attached File Attached
CPP-2020-papers16:18 - 16:40
Christian DoczkalUniversité Côte d'Azur, Damien PousCNRS, ENS Lyon
DOI Pre-print Media Attached