Paper: A constructive formalization of the catch and throw mechanism (at LICS 1992)

Authors: Hiroshi Nakano

Abstract

The catch/throw mechanism, a programming construct for nonlocal exit, plays an important role when programmers handle exceptional situations. A constructive formalization that captures the mechanism in the proofs-as-programs notion is given. A modified version of LJ equipped with inference rules corresponding to the operations of catch and throw is introduced. Then it is shown that one can actually extract programs that made use of the catch/throw mechanism from proofs under a certain realizability interpretation. Although the catch/throw mechanism provides only a restricted access to the current continuation, the formulation remains constructive

BibTeX

  @InProceedings{Nakano-Aconstructiveformal,
    author = 	 {Hiroshi Nakano},
    title = 	 {A constructive formalization of the catch and throw mechanism},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {82--89},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }