Asynchronous Exceptions as an Effect

William L. Harrison; Gerard Allwein; Andy Gill; Adam Procter

doi:10.1007/978-3-540-70594-9_10

Asynchronous Exceptions as an Effect

William L. Harrison
, Gerard Allwein
, Andy Gill
, Adam Procter

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

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 modular 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.

Original language	English
Title of host publication	Proceedings of the Mathematics of Program Construction (MPC08)
Pages	153-176
Number of pages	24
DOIs	https://doi.org/10.1007/978-3-540-70594-9_10
State	Published - 2008
Externally published	Yes

Access to Document

10.1007/978-3-540-70594-9_10

Cite this

@inproceedings{b608f0d28e224ee4bc8142c2b62f55af,

title = "Asynchronous Exceptions as an Effect",

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 modular 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.",

author = "Harrison, \{William L.\} and Gerard Allwein and Andy Gill and Adam Procter",

year = "2008",

doi = "10.1007/978-3-540-70594-9\_10",

language = "English",

pages = "153--176",

booktitle = "Proceedings of the Mathematics of Program Construction (MPC08)",

}

TY - GEN

T1 - Asynchronous Exceptions as an Effect

AU - Harrison, William L.

AU - Allwein, Gerard

AU - Gill, Andy

AU - Procter, Adam

PY - 2008

Y1 - 2008

N2 - 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 modular 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.

AB - 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 modular 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.

U2 - 10.1007/978-3-540-70594-9_10

DO - 10.1007/978-3-540-70594-9_10

M3 - Conference contribution

SP - 153

EP - 176

BT - Proceedings of the Mathematics of Program Construction (MPC08)

ER -

Asynchronous Exceptions as an Effect

Abstract

Access to Document

Fingerprint

Cite this