@inproceedings{WalterEA05,
  abstract = {Following the paradigm of encapsulation of side effects via monads, the
Java execution mechanism has been described by the so-called Java monad,
encorporating essentially stateful computation and exceptions, which are
heavily used in Java control flow. A technical problem that appears in
this model is the fact that the return exception in Java is parametrized
by the return value, so that method calls actually move between slightly
different monads, depending on the type of the return value. We provide
a treatment of this problem in the general framework of exception monads
as introduced in earlier work by some of the authors; this framework
includes generic partial and total Hoare calculi for abrupt
termination. Moreover, we illustrate this framework by means of a
verification of a pattern match algorithm.
},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {Walter, Dennis and Schr{\"o}der, Lutz and Mossakowski, Till},
  biburl = {https://www.bibsonomy.org/bibtex/2fd7cbcc0e81f9a7e57226e9a125ec77e/tillmo},
  booktitle = {Algebra and Coalgebra in Computer Science},
  editor = {Fiadeiro, Jose and Rutten, Jan},
  interhash = {2b15ccb149cc0bf675f60d1f30ae7126},
  intrahash = {fd7cbcc0e81f9a7e57226e9a125ec77e},
  isbn = {3-540-28620-9},
  keywords = {HasCASL calls exceptions java method monads},
  pages = {424-438},
  pdfurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/paramexc.pdf},
  psurl = {http://www.informatik.uni-bremen.de/~lschrode/papers/paramexc.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 = {Parametrized Exceptions},
  url = {http://www.springerlink.com/(bt4qw245oavupgzdxw3zpuul)/app/home/contribution.asp?referrer=parent&backto=searchcitationsresults,2,2;},
  volume = 3629,
  year = 2005
}