Väljaanne: Proceedings of the 20th International Symposium on Logical and Semantic Frameworks, with Applications, LSFA 2025, Brasília, Brazil, 6-11 October 2025
Autorid: De Pascalis, Michele; Uustalu, Tarmo; Veltri, Niccolò
Projekt uurib uusi sõltuvate tüüpidega tüübisüsteme, mis on sobilikud programmeerimiskeelte semantikate arendamiseks ja formaliseerimiseks tõestusassistentide abil. Eriline rõhk on keeltel, mis toetavad konkurentsust ja mittedetermiminismi, nt oleku-siirdesüsteemid ja protsessiarvutused. Populaarsed tüübiteoreetilised tõestusassistendid nagu Agda ja Coq ei sobi niisuguste keelte denotatsioonsemantika esitamiseks, kuna nende tüübisüsteemid ei ole piisavalt väljendusvõimsad. Me vastame sellele väljakutsele sel moel, et toome kaasaegsetesse tüübiteoreetilistesse raamistutesse nagu homotoopiline tüübiteooria sisse uue klassi koinduktiivseid tüüpe, mis esitavad saavutatavate funktorite terminaalseid koalgebraid. Denotatsioonsemantikas läheb protsesside mittedeteministliku ja interageeruva käitumise esitamiseks vaja tüüpe just sellest klassist. Loodavad väljendusvõimsamad tüübisüsteemid lubavad konkurentsuse ja mittedeterminismiga keelte formaalset semantikat adekvaatselt kodeerida.