Two Extensions of PX system (extended abstract)

作     者：Hayashi, Susumu Ishikawa, Masakazu Kobayashi, Satoshi Nakano, Hiroshi Nakazaki, Syuichi 

作者机构：Department of Computers Systems Engineering Kobe University Kobe Japan Department of Informatics Applied Mathematics Ryukoku University Ohtsu Japan Nissay Computer Co. Ltd. Osaka Japan Hyogo University code Kakogawa Japan 

出 版 物：《Electronic Notes in Theoretical Computer Science》 (Electron. Notes Theor. Comput. Sci.)

年 卷 期：1996年第3卷第C期

页      面：88-88页

学科分类：0810[工学-信息与通信工程] 0808[工学-电气工程] 08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Ministry of Education No06680333 

摘      要：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. © 1996 Elsevier B.V. All rights reserved.