@inproceedings{Async08,
  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},
  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.}
}