Resumen de lecturas compartidas durante febrero de 2020

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas, durante febrero de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante febrero de 2020”

Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq/Ssreflect sobre grafos titulado Graph theory in Coq: minors, treewidth, and isomorphisms.

Sus autores son

  • Christian Doczkal (Université Côte d’Azur, Inria Sopia Antipolis Méditerranée, France) y
  • Damien Pous (Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France).

Su resumen es

We present a library for graph theory in Coq/Ssreflect. This library covers various notions on simple graphs, directed graphs, and multigraphs. We use it to formalise several results from the literature: Menger’s theorem, the excluded-minor characterization of treewidth-two graphs, and a correspondence between multigraphs of treewidth at most two and terms of certain algebras.

El trabajo se ha publicado en el Journal of Automated Reasoning

El código de las correspondientes teorías se encuentra aquí.

Resumen de lecturas compartidas del 22 al 29 de febrero de 2020

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas, del 22 al 29 de febrero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

Read More “Resumen de lecturas compartidas del 22 al 29 de febrero de 2020”