{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:29:13Z","timestamp":1777645753392,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"2","license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2010,8]]},"abstract":"<jats:p>In the modern, multi-threaded, multi-core programming environment, correctly managing system resources, including locks and shared variables, can be especially difficult and errorprone. A simple mistake, such as forgetting to release a lock, can have major consequences on the correct operation of a program, by, for example, inducing deadlock, often at a time and location that is isolated from the original error. In this paper, we propose a new type-based approach to resource management, based on the use of dependent types to construct a Domain-Specific Embedded Language (DSEL) whose typing rules directly enforce the formal program properties that we require. In this way, we ensure strong static guarantees of correctness-by-construction, without requiring the development of a new special-purpose type system or the associated special-purpose soundness proofs. We also reduce the need for \u201cover-serialisation\u201d, the overly-conservative use of locks that often occurs in manually constructed software, where formal guarantees cannot be exploited. We illustrate our approach by implementing a DSEL for concurrent programming and demonstrate its applicability with reference to an example based on simple bank account transactions.<\/jats:p>","DOI":"10.3233\/fi-2010-303","type":"journal-article","created":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T23:13:13Z","timestamp":1575328393000},"page":"145-176","source":"Crossref","is-referenced-by-count":7,"title":["Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols"],"prefix":"10.1177","volume":"102","author":[{"given":"Edwin","family":"Brady","sequence":"first","affiliation":[{"name":"School of Computer Science, University of St Andrews, Jack Cole Building, North Haugh, St Andrews, Fife KY16 9SX, United Kingdom. {eb,kh}@cs.st-andrews.ac.uk"}]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of St Andrews, Jack Cole Building, North Haugh, St Andrews, Fife KY16 9SX, United Kingdom. {eb,kh}@cs.st-andrews.ac.uk"}]}],"member":"179","published-online":{"date-parts":[[2010,1]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2010-303","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2010-303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:33:12Z","timestamp":1777444392000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2010-303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,8]]}},"alternative-id":["10.3233\/FI-2010-303"],"URL":"https:\/\/doi.org\/10.3233\/fi-2010-303","relation":{"is-cited-by":[{"id-type":"doi","id":"10.4204\/EPTCS.291.5","asserted-by":"object"}]},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,1]]}}}