AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

60 Minutes

Saarbrücken

Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages.
In this paper we introduce an affine bounded linear typing discipline on a general notion of resource which can be modeled in a semiring.
For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational
theory, and a (coherent) categorical semantics. This is a very useful type-theoretic and denotational framework for many applications to
resource-sensitive compilation, and it represents a generalization of several existing type systems. As a non-trivial instance, motivated by
our ongoing work on hardware compilation, we present a complex new application to calculating and controlling timing of execution in a
(recursion-free) higher-order functional programming language with local store.

Dan R. Ghica, Alex Smith

Brigitta Hansen

0681 93039102

--email hidden

Yes

Kaiserslautern

G26

112

passcode not visible

logged in users only