A constructive logic behind the catch and throw mechanism
type: Item
instance of: scholarly article
title: A constructive logic behind the catch and throw mechanism
zbMATH Open document ID: 0815.03019
DOI: 10.1016/0168-0072(94)90087-6
author: Hiroshi Nakano
published in: Annals of Pure and Applied Logic
publication date: 1994-11-08T00:00:00Z
review text: The paper presents a typing system which captures the catch/throw mechanism (a programming construct for non-local exit) in the proofs-as- programs notion. The typing system is regarded as a constructive logic with facilities for exception handling. The catch/throw mechanism is handled in a natural deduction style formation in which a direct correspondence between proofs and programs can be seen. A simple programming language is defined and its operational semantics is given by a set of reduction rules. The author also introduces an abstract machine which can imitate the standard implementation of the catch/throw mechanism. To give a realizability interpretation to each typing judgement, only the fixed evaluation (call-by-value) strategy is considered. Problems of treating the catch/throw mechanism in a more general context remain unsolved. The investigation of the relationship between this mechanism and proof transformations would be an interesting problem as well.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68N15
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 683709
zbMATH Keywords: error handling
zbMATH Keywords: sequent calculus
zbMATH Keywords: typing system
zbMATH Keywords: catch/throw mechanism
zbMATH Keywords: proofs-as-programs notion
zbMATH Keywords: constructive logic
zbMATH Keywords: programming language
zbMATH Keywords: operational semantics
zbMATH Keywords: abstract machine
reviewed by: Marie Duží
describes a project that uses: LISP
MaRDI profile type: Publication
full work available at URL: 0168-0072(94)90087-6
OpenAlex ID: W2077187450
cites work: Q4174692
cites work: A syntactic theory of sequential control
cites work: The Mechanical Evaluation of Expressions
cites work: Eine Darstellung der Intuitionistischen Logik in der Klassischen
cites work: Call-by-name, call-by-value and the \(\lambda\)-calculus
cites work: Q5538910
cites work: Q3997095
cites work: Proof theory. 2nd ed
description: scientific article; zbMATH DE number 683709