W. L. Harrison, G. Allwein, A. Gill, and A. Procter, “Asynchronous exceptions as an effect,” in Ninth International Conference on Mathematics of Program Construction, Springer-Verlag, July 2008.

Links

• http://www.ittc.ku.edu/csdl/fpg/files/Harrison-08-Asynchronous.pdf

Abstract

Asynchronous interrupts abound in computing systems, yet they remain a thorny concept for both programming and verification practice. The ubiquity of interrupts underscores the importance of developing programming models to aid the development and verification of interrupt-driven programs. The research reported here recognizes asynchronous interrupts as a computational effect and encapsulates them as a building block in modular monadic semantics. The resulting integrated semantic model can serve as both a guide for functional programming with interrupts and as a formal basis for reasoning about interrupt-driven computation as well.

BibTeX

@inproceedings{Harrison:08:Asynchronous,
  author = {William L. Harrison and Gerard Allwein and Andy Gill and Adam Procter},
  title = {Asynchronous Exceptions as an Effect},
  booktitle = {Ninth International Conference on Mathematics of Program Construction},
  year = {2008},
  month = {July},
  publisher = {Springer-Verlag},
}