著者
岩間 太 小林 直樹
出版者
一般社団法人日本ソフトウェア科学会
雑誌
コンピュータソフトウェア (ISSN:02896540)
巻号頁・発行日
vol.19, no.2, pp.58-64, 2002-03-15

プログラミング言語Javaの仮想機械では,実行前にコードの検証を行い,不正なコードを排除している.しかし,現在の検証器では,並行スレッドによるロックの獲得・解放の整合性に関する検証は行っていない.この問題を解決するため,本研究では,AbadiとStataによるバイトコード検証のため型システムを改良する.新しい型システムでは,各オブジェクトのロックが獲得・解放される順序の情報をオブジェクトの型に付加することにより,ロックの正しい使用を保証する.
著者
小林 直樹
巻号頁・発行日
1995 (Released:1995-04-01)

本年度はまず、すでに我々が提案していた線形論理に基づく並列計算の枠組であるACLを高階に拡張したHACLを提案し、その意味論・型システム等を与え、静的に型づけされた(HACLで書かれた)並列プログラムが実行時に型エラーを起こさない等の基本的な性質を証明した。また、それに基づいたインタプリタの処理系を作成して、HACLの特徴の一つである(多相型をもった)高階プロセスが非常に有効であることをプログラミングを通して確認した。さらに、HACLの上に、インヘリタンスをはじめとする種々の機能を備えた並列オブジェクト指向言語を実現でき、かつそのようにして実現された並列オブジェクト指向言語で書かれたプログラムがHACLの型システムをとおして型推論・型チェックが行なえることを示した。その副産物として、型推論をとおして並列オブジェクトのメソッドのディスパッチが定数コストで行なえるようにコンパイルできることも示した。これらの結果に基づいて実際に、並列オブジェクト指向言語のプログラムからHACLへのトランスレータのプロトタイプも作成した。また、HACLを含めた非同期通信に基づく並列言語の効率のよい実現のために、エフェクト解析の手法を応用した並列プログラムの通信に関する解析を行なう方法を提案し、HACLを通した定式化・基本的な性質の証明・解析システムのプロトタイプの実装を行なった。将来的にはこの静的解析システムをコンパイラに組み込み、並列プログラムの最適化コンパイルに役立てる予定である。上記理論的側面の研究と並行してHACLに基づいた処理系の実装を進めており、現在シングルCPUのワークステーション用のコンパイラのプロトタイプがほぼ完成した状況である。
著者
長尾 大道 小林 直樹 深尾 良夫 冨澤 一郎 樋口 知之
出版者
日本学術会議 「機械工学委員会・土木工学・建築学委員会合同IUTAM分科会」
巻号頁・発行日
pp.47-47, 2012 (Released:2012-03-28)

大地震が起こった際には、それによって励起された波動が電離層内を伝搬していくことが、観測的に示されている。著者はこれまでに、固体地球‐大気結合系1次元モデルのノーマルモードを利用した数値シミュレーションにより、2008年に起こった岩手・宮城内陸地震によって励起された気圧変動を説明することに成功した。本研究では同じ手法を用いることにより、やはり同地震の際に菅平のHFドップラー観測で捉えられた電離層の上下変動を、中性大気を伝搬する音波波動として理解できることを示した。講演においては、他の地震の場合に得られたさらに多くの観測点で得られたHFドップラーデータを総合的に解析することにより、大地震によって励起される大気変動の時空間構造を包括的に理解することを目指す。
著者
小林 直樹 五十嵐 淳 田浦 健次朗 渡部 卓雄
巻号頁・発行日
1999 (Released:1999-04-01)

本研究の目的は,本研究代表者が提唱した疑似線形型システムに基づく新しいメモリ管理方式の実現により,プログラミング言語処理系のメモリ管理の信頼性および効率を改善することであった.主要な成果は以下のとおり.・擬似線形型システムに基づく型推論によるメモリの獲得・解放命令の挿入…擬似線形型システムに基づき,プログラム中で用いられる各データが最後に使用される箇所を特定し,その部分にメモリの解放命令を挿入するための方法を確立し,関数型言語MLを対象としてプロトタイプシステムを構築した.・擬似線形型システムに基づくメモリ管理のためのバイトコード言語の設計と実装…上で述べたメモリの獲得・解放命令を挿入したプログラムを実際に実行するためのバイトコード言語を設計し,実装を行った.・通常のメモリ管理の改良と本メモリ管理方式との融合…擬似線形型システムのみでは自動的に管理できないメモリが存在するため,既存のメモリ管理方式であるGCを改良して融合する方法について研究した.主な課題はGC自体の性能,特に並列計算機上のGCの性能をあげること,および疑似線形型に基づくメモリ管理によるダングリングポインタの問題の解決であった.後者については型情報を実行時まで保存し,GC時にこれを用いることによってこの問題を解決した.・線形型解析の資源使用解析への一般化…疑似線形型を拡張し,ファイルやネットワークなど一般の計算資源の使用方法の解析を行うための型システムを構築した.これにより(i)割り当てられたメモリはいずれ解放され,解放後はアクセスされない,(ii)オープンされたファイルはいずれクローズされ,クローズ後は読み書きされない,といった性質が満たされているかを統一的に検証することができる.
著者
柴田 昇 神田 和重 久田 俊記 磯部 克明 佐藤 学 清水 有威 清水 孝洋 杉本 貴宏 小林 智浩 犬塚 和子 金川 直晃 梶谷 泰之 小川 武志 中井 潤 岩佐 清明 小島 正嗣 鈴木 俊宏 鈴木 裕也 境 新太郎 藤村 朋史 宇都宮 裕子 橋本 寿文 御明 誠 小林 直樹 稲垣 泉貴 松本 勇輝 井上 諭 鈴木 良尚 何 東 本多 泰彦 武者 淳二 中川 道雄 本間 充祥 安彦 尚文 小柳 勝 吉原 正浩 井納 和美 野口 充宏 亀井 輝彦 加藤 洋介 財津 真吾 那須 弘明 有木 卓弥 Chibvongodze Hardwell 渡邉 光恭 丁 虹 大熊 直樹 山下 竜二 Liang Guirong Hemink Gertjan Moogat Farookh Trinh Cuong 東谷 政昭 Pham Tuan 金澤 一久
出版者
一般社団法人電子情報通信学会
雑誌
電子情報通信学会技術研究報告. ICD, 集積回路 (ISSN:09135685)
巻号頁・発行日
vol.112, no.15, pp.1-5, 2012-04-16

世界最小の19nmのデザインルールを用いて64Gb多値(2bit/cell)NANDフラッシュメモリを開発した。片側All-bit-Line S/A構成、1plane構成によりチップサイズは112.8mm^2。ビット線バイアスアクセラレーション及び"BC"State-First書込みアルゴリズムにより、書き込みパフォーマンスは15MB/sを実現。プログラムサスペンド機能とイレーズサスペンド機能により、リードレイテンシー時間は大幅に短縮。400Mb/s/pin 1.8Vの高速Toggle mode InterfaceをNANDフラッシュメモリとしては初めて搭載した。
著者
白石 浩章 山田 竜平 石原 吉明 小林 直樹 鈴木 宏二郎 田中 智
出版者
日本惑星科学会
雑誌
遊・星・人 : 日本惑星科学会誌 (ISSN:0918273X)
巻号頁・発行日
vol.21, no.3, pp.283-288, 2012-09-25
参考文献数
15

多点ネットワークを構成して火星表層環境および内部構造を観測するペネトレータミッションを提案する.現在の火星内部で生じているダイナミクスを反映する地震活動度と熱的状態を調査するとともに,地球型惑星の分化過程を反映する地殻-上部マントル構造と固体内部から表層および大気層への物質輸送過程に関する知見を得ることを目的とする.ペネトレータモジュールは突入速度300m/secで火星表層下2〜3mに潜り込むプローブ本体に,耐熱シールドと空力減速機構の役割をする膜面展開型柔構造エアロシェルを統合することで小型軽量なシステムを構成する.周回衛星から分離された4機のペネトレータは,火成活動の可能性が指摘されるElysium地域に最大300km間隔のネットワークを構成して地震観測や熱流量観測を行う.一方,柔構造エアロシェルには圧力計,温度計,磁力計,カメラを搭載して大気突入時のモニタリングを行う.
著者
永田 章人 小林 直樹 米澤 明憲
出版者
日本ソフトウェア科学会
巻号頁・発行日
pp.7, 2003 (Released:2003-12-17)

型付き言語MLにおけるメモリ管理手法として,リージョン推論に基づく方式がTofteらによって提案,実装されている.この手法では,通常のMLの型システムにメモリ情報(リージョン)を付加して拡張した型システムに基づいて型推論を行うことで,各オブジェクトの生存区間を推定し,メモリの解放・獲得のためのコードをコンパイル時に挿入する.リージョンに基づくメモリ管理は,ガーベジコレクションに比べて早期にオブジェクトを解放でき,また,参照カウントによるメモリ管理方式に比べて実行時のオーバーヘッドが少ない.しかしながら,リージョン推論はMLの静的な型推論の拡張であるため,他の言語,特にSchemeのように動的に型付けされた言語に適用できるかどうかは自明でなかった.本研究では,CartwrightらのSoft typeとリージョン付き型システムとを統合することにより,動的型付き言語に対してもリージョン推論に基づくメモリ管理が行なえることを示す.
著者
嵯峨田 淳 八島 由幸 小林 直樹
出版者
一般社団法人情報処理学会
雑誌
情報処理学会研究報告オーディオビジュアル複合情報処理(AVM) (ISSN:09196072)
巻号頁・発行日
vol.2000, no.24, pp.25-30, 2000-03-03
参考文献数
7
被引用文献数
1

従来のゼロツリー符号化はゼロツリールートの出現確率が極めて高いため,単純に可変長符号化した場合,そのエントロピーと比較して効率が低下する.このため,各シンボルの符号化には,一般的に算術符号化が用いられる.また,ゼロツリー符号化はその符号体系自体に冗長性があり,親子係数間の相関を効率的に除去できないという問題がある.本稿では,ある変換係数の直接の子供係数のうち,この子供係数がZTRである個数と,変換係数のレベルの絶対値からなる二次元可変長符号を用いてエントロピー符号化を行う.本手法により,解像度スケーラビリティを有しつつ,符号化効率を損なうことなく,可変長符号化を用いてウェーブレット変換係数を符号化することができる.This paper describes an efficient and effective entropy coding strategy for the compression of wavelet transformed, motion compensated prediction residuals. The proposed entropy coding algorithm consists of two dimensional variable length coding(2D-VLC), which encodes both the level of transformed coefficient and and the number of ZTRs in its direct children-coefficients simultaneously. At this time, 2×2 cluster of adjacent wavelet coefficients are jointly coded with the 2D-VLC to exploit the spatial correlation of neighboring coefficients. Along with the 2D VLCs of each cluster, the proposed zerotree-map code is appended at the head of them to remove the redundancies of any conventional zerotree encoding algorithms. Simulation results show that the proposed coding method is superior to conventional arithmetic coding, or variable length coding with the length ZTR runs.
著者
羽生 宏人 和田 英一 丹羽 崇博 近藤 靖雄 川村 尚史 丸山 信也 岡村 彩乃 山科 早英良 永井 康仁 中道 達也 上道 茜 田中 成明 小林 直樹 笠原 次郎 森田 泰弘
出版者
一般社団法人 日本航空宇宙学会
雑誌
航空宇宙技術 (ISSN:18840477)
巻号頁・発行日
vol.9, pp.15-21, 2010 (Released:2010-05-14)
参考文献数
6

The educational hybrid-rocket was successfully launched and it also landed within the predicted area. Aerodynamic characteristics of the rocket designed by students of Tsukuba University were evaluated by the wind tunnel testing with the support of Tokai University. The flight path affected by the environmental condition, especially wind direction and velocity, was simulated with the original calculation program. The altitude of the rocket was measured with the optical equipment and the apex was 123 m although the calculation indicated 198 m. We expected that the insufficient filling or the volatilization of Nitrous oxide as an oxidizer led to this result. And then, the apex was verified with a function of the oxidizer filling ratio. The results showed that 81.2 % of the oxidizer volume in comparison with the firing test condition was accumulated in the tank at the launch.
著者
大谷 栄治 倉本 圭 今村 剛 寺田 直樹 渡部 重十 荒川 政彦 伊藤 孝士 圦本 尚義 渡部 潤一 木村 淳 高橋 幸弘 中島 健介 中本 泰史 三好 由純 小林 憲正 山岸 明彦 並木 則行 小林 直樹 出村 裕英 大槻 圭史
出版者
日本惑星科学会
雑誌
遊・星・人 : 日本惑星科学会誌 (ISSN:0918273X)
巻号頁・発行日
vol.20, no.4, pp.349-365, 2011-12-25
被引用文献数
1

「月惑星探査の来たる10年」検討では第一段階で5つのパネルの各分野に於ける第一級の科学について議論した.そのとりまとめを報告する.地球型惑星固体探査パネルでは,月惑星内部構造の解明,年代学・物質科学の展開による月惑星進化の解明,固体部分と結合した表層環境の変動性の解明,が挙げられた.地球型惑星大気・磁気圏探査パネルは複数学会に跨がる学際性を考慮して,提案内容に学会間で齟齬が生じないように現在も摺り合わせを進めている.本稿では主たる対象天体を火星にしぼって第一級の科学を論じる.小天体パネルでは始原的・より未分化な天体への段階的な探査と,発見段階から理解段階へ進むための同一小天体の再探査が提案された.木星型惑星・氷衛星・系外惑星パネルは広範な科学テーマの中から,木星の大気と磁気圏探査,氷衛星でのハビタブル環境の探査,系外惑星でも生命存在可能環境と生命兆候の発見について具体的な議論を行った.アストロバイオロジーパネルでは現実的な近未来の目標として火星生命探査を,長期的な目標として氷衛星・小天体生命探査を目指した観測装置開発が検討された.これらのまとめを元に「月惑星探査の来たる10年」検討は2011年7月より第二段階に移行し,ミッション提案・観測機器提案の応募を受け付けた.
著者
小林 直樹 篠原 歩 五十嵐 淳 海野 広志
巻号頁・発行日
2015-05-29 (Released:2015-06-03)

本課題では、高階モデル検査の(1)理論とモデル検査アルゴリズム、(2)プログラム検証への応用、(3)データ圧縮への応用について研究を進めている。以下、それぞれについて、平成27年度の研究実績を述べる。(1)高階モデル検査の理論とモデル検査アルゴリズム:高階モデル検査アルゴリズムおよびその実装の改良を行った。その結果得られた新しい高階モデル検査器HorSat2は、標準のベンチマークについて従来の最速のモデル検査器よりも平均10倍程度の高速化を達成でき、単純な入力であれば数十万行の文法であっても一分程度で処理できる(従来の最速のモデル検査器では一万行程度が限界)ことを確認した。(2)プログラム検証への応用:高階モデル検査に基づくプログラム検証の新しい応用として、プログラム等価性、公平停止性の検証手法の考案および実装を行った。後者については、公平停止性の検証を到達可能性問題に帰着する手法を考案し、昨年度までに構築ずみの高階モデル検査に基づく到達可能性問題検証器と組み合わせることによって公平停止性検証器を実装した。これにより、線形時相論理LTLで表現可能な任意の性質の自動検証が可能になった。また、プログラムの検証を関数単位に分割して検証することを可能にするため、詳細型検査問題を到達可能性問題に帰着して解く手法を考案・実装した。さらに、木構造処理プログラムの自動検証手法やホーン節に基づく詳細型推論手法の改良を行った。(3)データ圧縮への応用:木構造データを、それを生成する関数型プログラム(ラムダ式)の形に圧縮する方式について、得られたラムダ式をコンパクトなビット列に変換する方法について引き続き改良を行い、(より表現力の弱い体系なので原理的にはよりコンパクトな表現が可能である)straightline programのビット表現と遜色ない大きさのビット表現を得ることに成功した。
著者
塚田 武志 小林 直樹
出版者
情報処理学会
雑誌
情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
巻号頁・発行日
vol.4, no.2, pp.31-47, 2011-03-25

言語の包含判定問題とは,与えられた言語 L1 と L2 について L1 ⊆ L2 が成立するか否かを判定する問題であり,理論的な興味の対象であるだけでなく,プログラム検証などへの広い応用を持つ重要な問題である.この問題に関する既知の最も強い結果の 1 つが文脈自由言語と超決定性言語の包含判定の決定可能性である.このオリジナルの証明は,Greibach と Friedman によって与えられている.我々はこの問題に対して,小林らによって提案されている型に基づく言語の包含判定の手法を適用し,決定可能性に対する別証明を与えた.この手法は以下のような利点を持つ.(1) 部分型関係やポンプの補題などのよく知られた概念で理論が展開できる.(2) 型推論を効率的に行う方法は多数提案されており,それらを利用することができる.また,提案する証明は小林らのアイデアを正規言語よりも広いクラスに適用したはじめての例であり,その他の非正規言語クラスへの応用も期待される.The language containment problem, which asks whether L1 ⊆ L2 for given languages L1 and L2, is an important problem in the field of formal language theory and has a variety of applications including program verification. One of the strongest result about this problem is the decidability for the case where L1 and L2 are context free and superdeterministic languages respectively, originally proved by Greibach and Friedman. In this paper, we give a new proof of the decidability, inspired by Kobayashi's type-based approach to language containment problems. The new proof has the following advantages. (1) The key notions and lemmas in the proof are well-known ones, such as subtyping and Pumping Lemma. (2) We can apply well-studied techniques for efficient typability checking. Furthermore, our proof is the first application of the type-based approach to the inclusion between non-regular languages and it seems applicable to other cases.
著者
岡田 光弘 小林 直樹 照井 一成 田村 直之
巻号頁・発行日
2003 (Released:2003-04-01)

次の3点を中心に研究を進めた。1.証明論と意味論の統合的見方について研究を進めた。カット消去定理等の証明論の基本定理の成立条件がPhase semanticsによる意味論的分析により明らかになることを示した。又、Simple logic等の線形論理の基礎理論に対して、証明論と意味論の統合を進めた。さらに、直観主義論理Phase semanticsと古典論理Phase semanticsとの密接な関係を明らかにした。Phase semanticsの成果に基づいてカット消去定理の意味論的条件の研究を進めた。2.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の確立に向けた研究を進めた。ゲーム論的意味論等の観点からの分析も加えた。(岡田・Girard等フランスグループとの共同研究)これまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にするLudics等の新たな論理体系理論の分析をGirardグループらと共同で行なった。3.線形論理的概念がプログラミング言語理論やソフトウェア形式仕様・検証理論、計算量理論等にどのように応用され得るかのケーススタディーを行なった。例えば昨年に引き続き、ダイナミック実時間システムのシステマティックな設計・検証や認証プロトコル安全性証明等を例にとり、線形論理的観点や手法の応用可能性を示した。この目的でフランス及び米国共同研究グループとの共同研究を行なうとともに、計3回の成果報告会を日仏共同で行った。
著者
荒木 領 小林 直樹 大野 光平 伊丹 誠
出版者
一般社団法人映像情報メディア学会
雑誌
映像情報メディア学会技術報告 (ISSN:13426893)
巻号頁・発行日
vol.36, no.10, pp.41-44, 2012-02-17
被引用文献数
1

ワンセグメントサービスは,日本における地上波デジタル放送の移動体向けのサービスである.しかし,使用帯域の狭さからマルチパスによるディップの影響を受けやすくなり,受信特性の劣化する可能性がある.この対策として,アンテナダイバーシティ技術がある.しかし,携帯電話などの小型のワンセグ受信機では,端末内に複数のアンテナを十分なダイバーシティ利得が得られるほど離して配置するのは不可能である.そこで,本稿では3台の受信端末を用いて受信情報を共有する協調受信を提案する.提案方式では,協調受信に用いる受信端末の台数を増やすことでワンセグメントサービスの誤り率特性が改善できることを示す.
著者
松村 千鶴 雨宮 加奈 雨宮 さよ子 雨宮 昌子 雨宮 良樹 板垣 智之 市野沢 功 伊藤 拓馬 植原 彰 内野 陽一 大川 清人 大谷 雅人 角谷 拓 掃部 康宏 神戸 裕哉 北本 尚子 國武 陽子 久保川 恵里 小林 直樹 小林 美珠 斎藤 博 佐藤 友香 佐野 耕太 佐野 正昭 柴山 裕子 鈴木 としえ 辻沢 央 中 裕介 西口 有紀 服巻 洋介 吉屋 利雄 古屋 ナミ子 本城 正憲 牧野 崇司 松田 喬 松本 雅道 三村 直子 山田 修 山田 知佳 山田 三貴 山田 祥弘 山田 玲子 柚木 秀雄 若月 和道 鷲谷 いづみ
出版者
日本生態学会
雑誌
保全生態学研究 (ISSN:13424327)
巻号頁・発行日
vol.8, no.2, pp.175-180, 2003-12-30
被引用文献数
2

Flower visitations by both native and exotic bumblebee species were investigated at 21 monitoring sites in various regions of Japan in the spring and summer of 2002. The investigation was part of a long-term program that has been in progress since 1997 to monitor the invasion of an alien bumblebee, Bombus terrestris L. (Hymenoptera: Apidae). Flower visitation by B. terrestris was ascertained at two monitoring sites, one in Shizuoka and one in Hokkaido, where a large number of colonies of this species have been commercially introduced for agricultural pollination.