Browse DORAS
Browse Theses
Latest Additions
Creative Commons License
Except where otherwise noted, content on this site is licensed for use under a:

Types and verification for infinite state systems

Mendel-Gleason, Gavin (2012) Types and verification for infinite state systems. PhD thesis, Dublin City University.

Full text available as:

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


Server-like or non-terminating programs are central to modern computing. It is a common requirement for these programs that they always be available to produce a behaviour. One method of showing such availability is by endowing a type-theory with constraints that demonstrate that a program will always produce some behaviour or halt. Such a constraint is often called productivity. We introduce a type theory which can be used to type-check a polymorphic functional programming language similar to a fragment of the Haskell programming language. This allows placing constraints on program terms such that they will not type-check unless they are productive. We show that using program transformation techniques, one can restructure some programs which are not provably productive in our type theory into programs which are manifestly productive. This allows greater programmer flexibility in the specification of such programs. We have demonstrated a mechanisation of some of these important results in the proof-assistant Coq. We have also written a program transformation system for this term-language in the programming language Haskell.

Item Type:Thesis (PhD)
Date of Award:November 2012
Supervisor(s):Hamilton, Geoff
Uncontrolled Keywords:Type-Theory; Type Checking; Provable Productivity
Subjects:Computer Science > Software engineering
DCU Faculties and Centres:Research Initiatives and Centres > Lero: The Irish Software Engineering Research Centre
DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing
Use License:This item is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 3.0 License. View License
Funders:SFI CSET Lero
ID Code:17152
Deposited On:15 Nov 2012 11:32 by Geoffrey Hamilton. Last Modified 15 Nov 2012 11:32

Download statistics

Archive Staff Only: edit this record