{"id":{"repo_id":"uwo","oai_identifier":"oai:uwo.scholaris.ca:20.500.14721/27376"},"canonical_url":"https://search.dev.ndltd.org/etd/uwo/oai:uwo.scholaris.ca:20.500.14721/27376","repository":{"repo_id":"uwo","name":"Western University","base_url":"https://uwo.scholaris.ca/server/oai/request"},"display":{"title":"Resource Bound Guarantees via Programming Languages","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Burrell, Michael J"],"institution":"The University of Western Ontario","degree_name":"Ph D","degree_level":null,"degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":["Mark Daley","James Andrews"],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-06-22","date_published":"2017-06-22","updated_at":"2026-07-27T21:56:14Z","subjects":["programming language","static analysis","resource bounds","type inference","polynomial time","time complexity","category theory"],"languages":["en_ca"],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/20.500.14721/27376","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Mark Daley","James Andrews"]},{"key":"dc:creator","label":"Author","values":["Burrell, Michael J"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2025-07-10T15:29:30Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2025-07-10T15:29:30Z"]},{"key":"dc:date.issued","label":"Date","values":["2017-06-22"]},{"key":"dc:publisher","label":"Institution","values":["The University of Western Ontario"]},{"key":"dc:type","label":"Dc Type","values":["thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph D"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["programming language","static analysis","resource bounds","type inference","polynomial time","time complexity","category theory"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en_ca"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/20.500.14721/27376"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["The thesis cover page in the PDF document includes references to Western University’s previous institutional repository platform, known as Scholarship@Western, and links to that platform (beginning with ir.lib.uwo.ca). In citing or referring to this thesis, use the DOI or handle from this page instead. Sample citation: Author name, \"Thesis title.\" (Year). Western University Open Repository. https://doi.org/10.71858/123456."]},{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["Resource Bound Guarantees via Programming Languages"]}]}],"canonical_facts":{"dc:contributor.advisor":["Mark Daley","James Andrews"],"dc:creator":["Burrell, Michael J"],"dc:date.accessioned":["2025-07-10T15:29:30Z"],"dc:date.available":["2025-07-10T15:29:30Z"],"dc:date.issued":["2017-06-22"],"dc:description":["The thesis cover page in the PDF document includes references to Western University’s previous institutional repository platform, known as Scholarship@Western, and links to that platform (beginning with ir.lib.uwo.ca). In citing or referring to this thesis, use the DOI or handle from this page instead. Sample citation: Author name, \"Thesis title.\" (Year). Western University Open Repository. https://doi.org/10.71858/123456."],"dc:description.abstract":["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."],"dc:identifier.uri":["https://hdl.handle.net/20.500.14721/27376"],"dc:language.iso":["en_ca"],"dc:publisher":["The University of Western Ontario"],"dc:subject":["programming language","static analysis","resource bounds","type inference","polynomial time","time complexity","category theory"],"dc:title":["Resource Bound Guarantees via Programming Languages"],"dc:type":["thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_name":["Ph D"]},"updated_at":"2026-07-27T21:56:14Z"}