ETD

• logic
• string diagrams
• tape diagrams

La tesi documenta lo sviluppo di un linguaggio domain-specific volto alla definizione, al rendering, e al controllo semi-automatico di proprietà di tape diagram, con applicazioni nell'ambito della verifica di programmi. Sono presentati due contributi teorici utili al fine dello sviluppo del tool: un encoding efficiente di string diagram di bicategorie cartesiane in formule della logica del primo ordine ed una procedura di normalizzazione di tape diagram con tracce che porta i diagrammi in Matrix-Within-Trace Normal Form. Questi risultati sono utilizzati nell'implementazione per facilitare il controllo automatico di inclusioni ed equivalenze tra tape diagram, e trovano applicazione concreta nel controllo di proprietà di programmi imperativi (e.g. validità di triple di Hoare). La realizzazione di questo tool è il primo passo verso lo sviluppo di TapeLab, un proof assistant grafico per tape diagram con capacità semi-automatiche.
---
The thesis documents the development of a domain-specific language aimed at the definition, rendering, and semi-automatic checking of properties of tape diagrams, with applications in program verification. Two theoretical contributions useful for the development of the tool are presented: an efficient encoding of string diagrams of cartesian bicategories into first-order logic formulas, and a normalization procedure for tape diagrams with traces that brings the diagrams into Matrix-Within-Trace Normal Form. These results are used in the implementation to facilitate the automatic checking of inclusions and equivalences between tape diagrams and have concrete applications in verifying properties of imperative programs (e.g., the validity of Hoare triples). The creation of this tool represents the first step toward the development of TapeLab, a graphical proof assistant for tape diagrams with semi-automatic capabilities.