Resource Bound Guarantees via Programming Languages

We present a programming language in which every well-typed program halts in time polynomial with respect to its input and, more importantly, in which upper bounds on resource requirements can be inferred with certainty. Ensuring that software meets its resource constraints is important in a number of domains, most prominently in hard real-time systems and safety critical systems where failing to meet its time constraints can result in catastrophic failure. The use of test- ing in ensuring resource constraints is of limited use since the testing of every input or environment is impossible in general. Static analysis, whether via the compiler or com- plementary programming tool, can generate proofs of correctness with certainty at the cost that not all programs can be analysed. We describe a programming language, Pola, which provides upper bounds on resource usage for well-typed programs. Further, we describe novel features of Pola that make it more expressive than existing resource-constrained programming languages.

Name thesis:degree_name

Ph D

Discipline thesis:degree_discipline

Computer Science

Grantor dc:publisher

The University of Western Ontario

Year dc:date.issued

2017

Author dc:creator

• Burrell, Michael J

Advisors dc:contributor.advisor

• Mark Daley
• James Andrews

• programming language
• static analysis
• resource bounds
• type inference
• polynomial time
• time complexity
• category theory

Language dc:language.iso

en_ca

Handle dc:identifier.uri

https://hdl.handle.net/20.500.14721/27376

OAI identifier oai:identifier

oai:uwo.scholaris.ca:20.500.14721/27376