Two Extensions of PX system (extended abstract)
Susumu Hayashi, M. K. Ishikawa, Satoshi Kobayashi, Hiroshi Nakano, Syuichi Nakazaki · Electronic Notes in Theoretical Computer Science · 1996
Two extensions of PX system will be discussed. The extensions are ctPX (catch/throw PX) and mvPX (multiple values PX). ctPX is a PX system extended with Nakano's catch/throw logic. ctPX enables to extract LISP programs with catch/throw mechanism form natural proofs. mvPX is a PX system which uses multiple values rather than lists to keep a finite sequences of data. Programs extracted by ctPX are more efficient than the ones by the original PX.