Locally Small Fibrationに基づく型体系

• Item type: SIG Technical Reports(1)
• 公開日: 1989-09-20
• タイトル: Locally Small Fibrationに基づく型体系
• タイトル / 言語: en
• タイトル: A Type System Based on Locally Small Fibration
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東京大学理学部情報科学科
• 著者所属(英): en
• 著者所属(英): Department of Information Science, University of Tokyo
• 著者名: 武山, 誠
• 著者名(英): Makoto, Takeyama
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では、依存型をもつ一階の型体系TFをLocally Small Fibrationという数学的構造に基づいて構築する。Categoricalにみて基本的な構造であるLSFが、type dependencyにおけるcontextの概念を完全に表現するものであることが示される。TFは一般化された項と依存型をもち、体系内に定義された代入操作を用いて変数なしの構文を実現している。また、依存積と依存和は完全な双対として扱われる。LSFは従来のtype dependencyのモデルを含み、対応するTFは従来の体系の自然な一般化である。従来のモデル、体系との関係についても考察する。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This article presents TF, a first order type system with dependent types based on a mathematical structure Locally Small Fibration. It is shown that LSF perfectly represents the concept of contexts of dependent types. TF has generalized notion of terms and dependent types, and enbodies a variable-free syntax with built-in substitution operators. TF's dependent products and coproducts are complete dual of each other. Since LSF is a natural generalization of other existing models of type dependency, TF is also that of existing systems. The relation between TF and these systems are examined.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1989, 号 75(1989-PRO-031), p. 1-10, 発行日 1989-09-20
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会