WEKO3
アイテム
A Second Order Typed Context Calculus
https://ipsj.ixsq.nii.ac.jp/records/16875
https://ipsj.ixsq.nii.ac.jp/records/168758be4db22-c2a1-4e27-97b8-92b3fdc0c558
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4207015.pdf (31.2 kB)
|
Copyright (c) 2001 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2001-07-15 | |||||||
| タイトル | ||||||||
| タイトル | A Second Order Typed Context Calculus | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Second Order Typed Context Calculus | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 発表概要 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| Graduate School of Informatics Kyoto University | ||||||||
| 著者所属 | ||||||||
| Graduate School of Informatics Kyoto University | ||||||||
| 著者所属 | ||||||||
| Graduate School of Informatics Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Informatics, Kyoto University | ||||||||
| 著者名 |
AzzaA.Taha
× AzzaA.Taha
|
|||||||
| 著者名(英) |
Azza, A.Taha
× Azza, A.Taha
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In this paper we introduce a second order context calculus $ｴlambda_{2xc}$ which has context as a first-class object and hole-filling as an explicit operation. In the representation of contexts both the term variable and the type variable can get bound after filling in the hole. In our calculus the holes of the contexts are represented by ordinary variables of appropriate types and hole-filling is represented by the usual application together with a new abstraction mechanism which represents the variables intended to be bound after filling in the hole. In order to avoid the unwanted-capture of variables during substitution the push and pull techniques are used to rename free variables instead of the usual $ｴalpha$-conversion which renames bound variables to avoid the unwanted capture of the free variables. A general definition for the push operator is introduced to avoid repeating essentially the same definitions for similar cases. We show that our calculus is confluent and the type system has the subject reduction property. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 42, 号 SIG07(PRO11), p. 91-91, 発行日 2001-07-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
