Diagrammatic Reasoning and Enhanced Static Constraints Export

@inproceedings{burton:draesc, abstract = {This paper reports on ongoing work to create a proof-carrying Domain Specific Embedded Language (DSEL) for diagrammatic logics, using Euler diagrams as a case study. The DSEL is written in Haskell with type system extensions that allow the exploitation of a combination of ideas from Constructive Type Theory. These extensions offer an increase in expressiveness over Hindley-Milner type systems and have been used for program verification. We use these extensions to create enhanced static constraints to enforce invariants on diagrams and transformations (inference rules). Our work is at an early stage and we describe the goals and challenges ahead. The major goal is to create a DSEL for generalized constraint diagrams, a visual logic expressive enough to be useful for modelling software, and to extract the types of the resulting diagrams for use as software artefacts.}, author = {Burton, James}, booktitle = {Proceedings of the 13th ESSLLI Student Session}, citeulike-article-id = {3401653}, editor = {Balogh, Kata}, keywords = {diagrams}, location = {Hamburg}, month = {August}, organization = {Association for Logic, Language and Information}, pages = {47--56}, posted-at = {2008-10-13 18:30:29}, priority = {0}, title = {Diagrammatic Reasoning and Enhanced Static Constraints}, year = {2008} }

TY - CONF ID - burton:draesc L3 - citeulike-article-id:3401653 N2 - This paper reports on ongoing work to create a proof-carrying Domain Specific Embedded Language (DSEL) for diagrammatic logics, using Euler diagrams as a case study. The DSEL is written in Haskell with type system extensions that allow the exploitation of a combination of ideas from Constructive Type Theory. These extensions offer an increase in expressiveness over Hindley-Milner type systems and have been used for program verification. We use these extensions to create enhanced static constraints to enforce invariants on diagrams and transformations (inference rules). Our work is at an early stage and we describe the goals and challenges ahead. The major goal is to create a DSEL for generalized constraint diagrams, a visual logic expressive enough to be useful for modelling software, and to extract the types of the resulting diagrams for use as software artefacts. CY - Hamburg OR - Association for Logic, Language and Information EP - 56 TI - Diagrammatic Reasoning and Enhanced Static Constraints T2 - Proceedings of the 13th ESSLLI Student Session SP - 47 KW - diagrams AU - Burton, James A2 - Balogh, Kata PY - 2008/08// ER -