Deciding Isomorphisms of Simple Types in Polynomial Time

The isomorphisms holding in all models of the simply typed lambda calculus with surjective and terminal objects are well studied - these models are exactly the Cartesian closed categories. Isomorphism of two simple types in such a model is decidable by reduction to a normal form and comparison under a finite number of permutations (Bruce, Di Cosmo, and Longo 1992). Unfortunately, these normal forms may be exponentially larger than the original types so this construction decides isomorphism in exponential time. We show how using space-sharing/hash-consing techniques and memoization can be used to decide isomorphism in practical polynomial time (low degree, small hidden constant). Other researchers have investigated simple type isomorphism in relation to, among other potential applications, type-based retrieval of software modules from libraries and automatic generation of bridge code for multi-language systems. Our result makes such potential applications practically feasible.

Extending snBench to Provide Concurrency Support in the Sensorium Execution Environment (SXE)

The SNBENCH is a general-purpose programming environment and run-time system targeted towards a variety of Sensor applications such as environmental sensing, location sensing, video sensing, etc. In its current structure, the run-time engine of the SNBENCH namely, the Sensorium Execution Environment (SXE) processes the entities of execution in a single thread of operation. In order to effectively support applications that are time-sensitive and need priority, it is imperative to process the tasks discretely so that specific policies can be applied at a much granular level. The goal of this project was to modify the SXE to enable efficient use of system resources by way of multi-tasking the individual components. Additionally, the transformed SXE offers the ability to classify and employ different schemes of processing to the individual tasks.