Fundamenta Informaticae - Volume 102, issue 2

Authors: Altenkirch, Thorsten | Uustalu, Tarmo

Article Type: Other

DOI: 10.3233/FI-2010-302

Citation: Fundamenta Informaticae, vol. 102, no. 2, pp. i-i, 2010

Authors: Brady, Edwin | Hammond, Kevin

Article Type: Research Article

Abstract: 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 “over-serialisation”, 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. Show more

DOI: 10.3233/FI-2010-303

Citation: Fundamenta Informaticae, vol. 102, no. 2, pp. 145-176, 2010

Authors: Löh, Andres | McBride, Conor | Swierstra, Wouter

Article Type: Research Article

Abstract: We present the type rules for a dependently typed core calculus together with a straight-forward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.

DOI: 10.3233/FI-2010-304

Citation: Fundamenta Informaticae, vol. 102, no. 2, pp. 177-207, 2010

Authors: Wilson, Sean | Fleuriot, Jacques | Smaill, Alan

Article Type: Research Article

Abstract: Writing dependently typed functional programs that capture non-trivial program properties is difficult in current systems due to lack of proof automation. We identify proof patterns that occur when programming with dependent types and detail how automating such patterns allow us to work more comfortably with types that capture, for example, membership, ordering and non-linear arithmetic properties. We describe the role of the rippling heuristic, both for inductive and non-inductive proofs, and generalisation in providing such automation. We then discuss an implementation of our ideas in Coq with practical examples of dependently typed programs, that capture useful program properties, which can …be verified automatically. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined functions and inductive data types. Show more

Keywords: Dependent types, rippling, generalisation, automated theorem proving, Coq

DOI: 10.3233/FI-2010-305

Citation: Fundamenta Informaticae, vol. 102, no. 2, pp. 209-228, 2010