A nyelv formális megközelítése
Erőteljes formális technikai munka áll a POOL2 tervezése mögött. Több szemantikai modellt és az egymással való kapcsolatukat vizsgálták. Jelentős előrehaladások vannak a programhelyesség formalizálásában. A szemantika definíciós módszerek közül az operációs és denotációs technikákat kell megemlíteni, de további definíciós módszereket is bevetnek. (pl. processz algebra, gráfnyelvtanok,...) Bebizonyították, hogy a nyelv operációs és denotációs módszerrel megadott szemantikája egymással ekvivalens. Fejlesztenek formális helyességbizonyítást is a nyelvhez, de ez még nehezebb, mint a formális szemantika megadása. Ezért a munkát több szintre osztották fel. Először a POOL szekvenciális változatának a SPOOL helyességbizonyítását tanulmányozzák. Ebben a nyelvben nincsenek törzsek, egy pillanatban csak egy aktív objektum van. Erre a nyelvre Hoare-féle helyességbizonyítást alkalmaztak. A fő eredményei, hogy a dinamikus pointer struktúrákat is tud kezelni a módszer és leírható vele pl. egy objektum létrehozása. Az üzenetküldés kezelése csak szekvenciális esetben van meg.