Un enfoque directo de razonamiento en torno a los programas concurrentes consiste en definir su comportamiento como un conjunto de todos los posibles entrelazamientos de las acciones atómicas de los subprocesos individuales. Sin embargo, razonar en términos de intercalaciones resulta demasiado difícil tanto para los humanos como para los ordenadores, porque el número de intercalaciones posibles crece rápidamente.

Los modelos de concurrencia no intercalados, como los lenguajes y las estructuras de eventos pomset, intentan abordar este problema proponiendo representaciones más compactas para el conjunto de comportamientos del programa. En los últimos años se ha renovado el interés por los modelos de concurrencia no intercalados, por ejemplo, en el contexto de los modelos de memoria relajados, la verificación de modelos de programas concurrentes y las pruebas de mutación basadas en modelos.

El objetivo de este proyecto es desarrollar una teoría mecanizada de modelos de concurrencia no intercalados en el Coq Proof Assistant. La biblioteca debería ayudar a los investigadores interesados a demostrar formalmente las propiedades de estos modelos y a desarrollar nuevas aplicaciones de la teoría.

Repositorio del proyecto