A framework for resource dependent EDSLs in a dependently typed language

de Muijnck-Hughes, Jan and Brady, Edwin and Vanderbauwhede, Wim; Hirschfeld, Robert and Pape, Tobias, eds. (2020) A framework for resource dependent EDSLs in a dependently typed language. In: 34th European Conference on Object-Oriented Programming, ECOOP 2020. Leibniz International Proceedings in Informatics, LIPIcs, 166 . Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, DEU. ISBN 9783959771542 (https://doi.org/10.4230/LIPIcs.ECOOP.2020.20)

[thumbnail of Muijnck-Hughes-etal-ECOOP2020-A-framework-resource-dependent-EDSLs-dependently-typed-language]
Preview
 Text. Filename: Muijnck-Hughes-etal-ECOOP2020-A-framework-resource-dependent-EDSLs-dependently-typed-language.pdf
Final Published Version
License: Creative Commons Attribution 3.0 logo
Download (598kB)| Preview

Abstract

Idris’ Effects library demonstrates how to embed resource dependent algebraic effect handlers into a dependently typed host language, providing run-time and compile-time based reasoning on type-level resources. Building upon this work, Resources is a framework for realising Embedded Domain Specific Languages (EDSLs) with type systems that contain domain specific substructural properties. Differing from Effects, Resources allows a language’s substructural properties to be encoded within type-level resources that are associated with language variables. Such an association allows for multiple effect instances to be reasoned about autonomically and without explicit type-level declaration. Type-level predicates are used as proof that the language’s substructural properties hold. Several exemplar EDSLs are presented that illustrates our framework’s operation and how dependent types provide correctness-by-construction guarantees that substructural properties of written programs hold.

  • Item type:Book Section
    ID code:87144
    Dates:
    Date
    Event
    6 November 2020
    Published
    8 April 2020
    Accepted
    Notes:Funding Information: Funding This work was funded by EPSRC projects: Border Patrol: Improving Smart Device Security through Type-Aware Systems Design (EP/N028201/1); and Type-Driven Verification of Communicating Systems – EP/N024222/1. Publisher Copyright: © Jan de Muijnck-Hughes, Edwin Brady, and Wim Vanderbauwhede.
    Subjects:Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:02 Nov 2023 13:39
    Last modified:23 Apr 2024 00:05
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/87144
CORE (COnnecting REpositories)