Using Dependent Types to Define Energy Augmented Semantics of Programs

Bernard van Gastel*, Rody Kersten, Marko van Eekelen

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


Energy is becoming a key resource for IT systems. Hence, it can be essential for the success of a system under development to be able to derive and optimise its resource consumption. For large IT systems, compositionality is a key property in order to be applicable in practice. If such a method is hardware parametric, the effect of using different algorithms or running the same software on different hardware configurations can be studied. This article presents a hardware-parametric, compositional and precise type system to derive energy consumption functions. These energy functions describe the energy consumption behaviour of hardware controlled by the software. This type system has the potential to predict energy consumptions of algorithms and hardware configurations, which can be used on design level or for optimisation.
Original languageEnglish
Title of host publicationFoundational and Practical Aspects of Resource Analysis
Subtitle of host publication4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers
EditorsMarko van Eekelen, Ugo Dal Lago
Place of PublicationCham
PublisherSpringer International Publishing AG
Number of pages20
ISBN (Electronic)9783319465593
ISBN (Print)9783319465586
Publication statusPublished - 2016
EventFoundational and Practical Aspects of Resource Analysis - London, United Kingdom
Duration: 11 Apr 201511 Apr 2015
Conference number: 4

Publication series

SeriesLecture Notes in Computer Science (LNCS) series


WorkshopFoundational and Practical Aspects of Resource Analysis
Abbreviated titleFOPARA 2015
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Using Dependent Types to Define Energy Augmented Semantics of Programs'. Together they form a unique fingerprint.

Cite this