%0 Conference Paper %1 SchroderMossakowski04 %A Schröder, Lutz %A Mossakowski, Till %B Algebraic Methodology and Software Technology %D 2004 %E Rattray, Charles %E Maharaj, Savitri %E Shankland, Carron %I Springer; Berlin; http://www.springer.de %K HasCASL Java dynamic exception logic monad %P 443--459 %T Generic exception handling and the Java monad %U http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3116&spage=443 %V 3116 %X We develop an equational definition of exception monads that characterizes Moggi's exception monad transformer. This axiomatization is then used to define an extension of previously described monad-independent computational logics by abnormal termination. Instantiating this generic formalism with the Java monad used in the LOOP project yields in particular the known Hoare calculi with abnormal termination and JML's method specifications; this opens up the possibility of extending these formalisms by hitherto missing computational features such as I/O and nondeterminism.

@inproceedings{SchroderMossakowski04, abstract = {We develop an equational definition of exception monads that characterizes Moggi's exception monad transformer. This axiomatization is then used to define an extension of previously described monad-independent computational logics by abnormal termination. Instantiating this generic formalism with the Java monad used in the LOOP project yields in particular the known Hoare calculi with abnormal termination and JML's method specifications; this opens up the possibility of extending these formalisms by hitherto missing computational features such as I/O and nondeterminism. }, added-at = {2016-08-05T15:59:03.000+0200}, author = {Schr{\"o}der, Lutz and Mossakowski, Till}, biburl = {https://www.bibsonomy.org/bibtex/2524e6808d01b79872627062a86210cd3/tillmo}, booktitle = {Algebraic Methodology and Software Technology}, editor = {Rattray, Charles and Maharaj, Savitri and Shankland, Carron}, interhash = {de5286482826df5cf979c730b1198e3d}, intrahash = {524e6808d01b79872627062a86210cd3}, keywords = {HasCASL Java dynamic exception logic monad}, pages = {443--459}, pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/javapdl.pdf}, psurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/javapdl.ps}, publisher = {Springer; Berlin; http://www.springer.de}, series = {Lecture Notes in Computer Science}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {Generic exception handling and the {J}ava monad}, url = {http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=3116&spage=443}, volume = 3116, year = 2004 }