Iris

Presentamos Iris, una lógica de separación concurrente con una premisa simple: los monoidales y los invariantes son todo lo que necesitas. Los monoidales conmutativos parciales nos permiten expresar—y los invariantes nos permiten hacer cumplir—los *protocolos* definidos por el usuario sobre el estado compartido, que están en el núcleo conceptual de la mayoría de las lógicas de programación recientes para la concurrencia. Además, a través de una nueva extensión del concepto de *cambio de vista*, Iris admite la codificación de *especificaciones lógicamente atómicas*, es decir, especificaciones al estilo de Hoare que permiten al cliente de una operación tratar la operación esencialmente como si fuera atómica, incluso si no lo es.