i-nth logo


Martin Erwig, Robin Abraham, Irene Cooperstein, & Steve Kollmansberger


Existing spreadsheet systems allow users to change cells arbitrarily, which is a major source of spreadsheet errors.

We propose a system that prevents errors in spreadsheets by restricting spreadsheet updates to only those that are logically and technically correct. The system is based on the concept of templates that describe the principal structure of the initial spreadsheet and all of its future versions.

We have developed a program generator that translates a template into an initial spreadsheet together with customized update operations for changing cells and inserting/deleting rows and columns for this particular template.

We have designed a type system for templates that ensures the following form of "spreadsheet maintenance safety": Update operations that are generated from a type-correct template are proved to transform the spreadsheet only according to the template and to never produce any omission, reference, or type errors.

Finally, we have developed a prototype as an extension to Excel, which has been shown by a preliminary usability study to be well accepted by end users.


Gencel system architecture
Gencel system architecture

The components of the Gencel system are shown in this figure.

The generator and type checker have been implemented in Haskell. The information from the Excel sheet being manipulated by the end user is captured by a VBA program and sent to the backend server.

The Haskell modules are compiled with GHC to a Windows executable that runs as the backend server.


2005, 27th ACM/IEEE International Conference on Software Engineering, May, pages 136-145

Full article

Automatic generation and maintenance of correct spreadsheets