サクサク読めて、アプリ限定の機能も多数！
トップへ戻る
ドラクエ3
www.sato.kuis.kyoto-u.ac.jp/~igarashi
ＭＬ型推論の光と影影 @@平成廿一年東都大駱駝会平成廿一年東都大駱駝会 京都大学 五十嵐 淳 自己紹介 情報科学の研究をしています 専門はプログラミング言語とか型理論とか 研究のひとつはJavaの改良ですが、Javaでプログラ ムは書きません(けません) ML歴16年、OCaml歴は11年くらい の著者です 小学生の解法 全員ラクダだとすると足の数は 4 x 7 = 28 本 実際には20本あるから8本分ラクダが多い ラクダ一匹をOCamlプログラマに置き換えると 足は2本減るから4人置き換えれば丁度よい OCamlプログラマ 4匹、ラクダ 3 匹 いきなり鶴亀算 OCamlプログラマとラクダが合わせて7匹いる。 足の数が合わせて20本である時、 OCamlプログラマとラクダはそれぞれ何匹いるか。 中学生の解法 OCamlプログラマの数を x、ラクダの数を y とすると、 x + y =
Featherweight Java のための漸進的型付け 伊奈 林太郎 1 五十嵐 淳 2 1 京都大学 工学部情報学科 ina@kuis.kyoto-u.ac.jp 2 京都大学 大学院情報学研究科 igarashi@kuis.kyoto-u.ac.jp 概 要 静的型システムと動的型システムの両者の利点を活かす枠組みとして, Siek と Taha は漸進的型付 けを提唱している. 漸進的型付けでは, 型宣言された部分のみ静的型検査が行なわれ, 残りの部分について は実行時検査が行なわれる. これにより, 当初型を付けずに書いたプログラムに型宣言を徐々に付加し, 静 的型付けされたプログラムを完成させることができる. 本研究では, 漸進的型付けをクラスに基づくオブ ジェクト指向言語で実現する理論的基盤として, Igarashi, Pierce, Wadler らの計算体系 Feat
講義内容(シラバスより) 数理論理学的手法を用いたソフトウェア科学の基礎理論について講述する．特に、 プログラミング言語の形式化と意味論、また，型システムとプログラムの安全性な ど，形式化を用いたプログラムの性質に関する議論をする． お知らせ 配布資料(12)改訂版を置きました．(2010.2.2) 配布資料(11),配布資料(12),最終レポート課題を置きました．(2010.2.1) 配布資料(10)を置きました．(2010.1.11) 配布資料(8)を改訂しました．(2010.1.10) 配布資料(9)を置きました．(2010.1.6) 配布資料(8)を置きました．(2010.1.5) 配布資料(7)を置きました．(2009.12.7) 中間レポート提出者には確認の返事を出しました．提出したにも関わらず， 確認の返事をもらっていない人は連絡を下さい．(2009.12.2) 配布資料(6
ここでは <式> の代わりに e という記号(メタ変数)，<識別子> の代わりに x という記号(メタ変数)を用いている． また，型(メタ変数 τ)として，整数を表す int, 真偽値を表す boolを考える． さて，型推論のアルゴリズムを考える前に，そもそも「式 e が型 τ を持つ」という関係がどのような時に成立するかを正確に記述したい． 例えば「式 1+1 は型 int を持つ」だろうが， 「式 if 1 then 2+3 else 4 は型 int を持つ」は 成立しないと思われる．この，「式 e が型 τ を持つ」 という判断を型判断(type judgment)と呼び，e : τ と略記する． しかし，一般に式には変数が現れるため，例えば単に x が int を持つか，といわれても判断することができない．このため，変数に対しては，そ れが持つ型を何か仮定しないと型判断は下せ
Objective Caml 入門 五十嵐 淳 京都大学 工学部情報学科計算機科学コース 大学院情報学研究科知能情報学専攻 e-mail: igarashi@kuis.kyoto-u.ac.jp October 24, 2002
担当授業 今年度 2008(夏) 工学部情報学科 計算機科学コース「技術英語」 2008(冬) 大学院情報学研究科 知能情報学専攻 ソフトウェア基礎論 2008(冬) 工学部情報学科 計算機科学コース 計算機科学実験及演習4(プログラム検証) 過去の授業 2007(夏) 全学共通科目新入生向け少人数セミナー(ポケットゼミ) 「再帰的思考とコンピュータプログラム」 2007(夏) 工学部情報学科 計算機科学コース「技術英語」 2007(冬) 大学院情報学研究科 知能情報学専攻 ソフトウェア基礎論 2007(冬) 工学部情報学科 計算機科学コース 計算機科学実験及演習4(プログラム検証) 2006(夏) 全学共通科目新入生向け少人数セミナー(ポケットゼミ) 「再帰的思考とコンピュータプログラム」 2006(冬) 大学院情報学研究科 知能情報学専攻 ソフトウェア基礎論 2006(冬) 工学部情報
3.11 いろいろな引数渡しの方式 — 値呼び・参照呼び・名前呼び・必要呼び 参照呼出し 遅延評価と call-by-need, call-by-name 前節までの言語では，値呼び出しに基づいて関数呼び出しの際の引数渡しを実 現してきた．本節では，FORTRAN, Pascal などに見られる 参照呼出し(call-by-reference)と，遅延評価(lazy evaluation)を使った， Algol60 に見られる 名前呼出し(call-by-name)，Haskell などに見 られる，必要呼出し(call-by-need)といった引数渡しの方法をみてい く． 3.11.1 参照呼出し 前節で説明したように，値呼出しの下では，関数のパラメータに対する代入は 関数呼出し側に影響をおよぼすことはない．つまり，関数呼出しの前後で，あ る変数の内容が変わることがなく，呼出し側・
技術評論社のこの本に関するページ 第16章のプログラム Makefile 盤面のサンプル: sample.board 補助関数定義: mySupport.mli, mySupport.ml 盤面のデータ構造定義: board.mli, board.ml 盤面定義ファイルの読み込み: input.mli, input.ml GUI とメインプログラム: gui.ml 補足・正誤表 -n 行目とあるのは，ページの下から n 行目のことです． p.28 日本語の使用について: 文字列定数中の Shift-JIS の使用に関して は問題がある，との指摘を東北大学の住井さんより頂きました(ありがとうご ざいます)．具体的には，文字列定数中で「ソ」「表」など，2バイト目に (ASCIIなら)バックスラッシュに対応する 5C が割り当てられている漢字を使 用した場合，コンパイラは2バイト文字を認識しませ
関連リンク 京都大学 大学院情報学研究科 知能情報学専攻 佐藤・五十嵐研究室 工学部情報学科計算機科学コース 東京大学 大学院情報理工学系研究科 コンピュータ科学専攻, 米澤研究室 大学院総合文化研究科 広域システム科学系 情報・図形 情報システム研究グループ 東北大学大学院情報科学研究科情報基礎科学専攻 小林研究室 University of Pennsylvania Department of Computer and Information Science Prof. Benjamin Pierce last update on $Date: 2008-09-22 14:53:53 +0900 (Mon, 22 Sep 2008) $
Objective Caml を始めとする関数型言語では，関数を整数・文字列などのデータと 同じように扱うことができる．すなわち，ある関数を， 他の関数への引数として渡したり，組などのデータ構造に 格納したりすることができる．このことを「Objective Caml では関数は第一級の値(first-class value)である」といい，また関数を引数/返り値とする ような関数を高階関数(higher-order function)と呼ぶ． まず，前回の復習をかねて，12 + 2 2 + ⋯ + n2 を計算する 関数 sqsum と，13 + 2 3 + ⋯ + n3 を計算する 関数 cbsum を定義してみよう． # let rec sqsum n = # if n = 0 then 0 else n * n + sqsum (n - 1) # let rec cbsum n =
2005年度「計算機科学実験及演習4(記号処理)」 実験資料 関数型プログラミング言語とインタプリタ 五十嵐 淳 京都大学 工学部情報学科計算機科学コース 大学院情報学研究科知能情報学専攻 工学部10号館1階142号室 e-mail: igarashi@kuis.kyoto-u.ac.jp
日本ソフトウェア科学会チュートリアル 「Java言語の最新事情」 Java 5.0 の新機能 五十嵐 淳 京都大学 大学院情報学研究科 igarashi@kuis.kyoto-u.ac.jp http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/ チュートリアルの内容 J2SE 5.0 において導入された新言語機能紹介 ジェネリクス ボクシングとアンボクシング イテレータ・配列のための for 文拡張 列挙(enum)型 可変長パラメータ 裏テーマ 「言語拡張 ＝ イディオムのコンパイラサ ポート」 イディオムへの自動展開 さらなる安全性チェック Java言語拡張の限界を暴く（？） 実装方式が及ぼす言語機能への影響 1.4から5.0へ public static void main(String[] args) { List lst = new Arr
参考図書 Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002. Robin Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999. igarashi@kuis.kyoto-u.ac.jp Last update on $Date: 2008-10-03 22:26:19 +0900 (Fri, 03 Oct 2008) $.
Featherweight Java: A Minimal Core Calculus for Java and GJ By Atsushi Igarashi, Benjamin Pierce and Philip Wadler. ACM Transactions on Programming Languages and Systems, 23(3):396-450, May 2001. A preliminary summary appeared in Proceedings of ACM Conference on Object-Oriented Programing, Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices, volume 34, number 10, pages 132-146, Den
What's New 2008年度ページ立ち上げ(2008.08.26) 「Objective Caml 入門」などを置きました(2008.10.01) 座学のスケジュールと課題1を追加しました(2008.10.02) FAQ Q: (コメントに)日本語を混ぜると #use で読み込めません． A: ファイルの文字コードを EUC-JP にしてください．Emacs であれば， C-x RET f euc-jp-unix としてください． 実験日程(目安) 日付範囲レポート課題
Objective Caml 入門五十嵐 淳 京都大学 工学部情報学科計算機科学コース 大学院情報学研究科知能情報学専攻 e-mail: igarashi@kuis.kyoto-u.ac.jp September�24, 2007 Contents Chapter�1�� 1.1��関数型言語 ML と Objective Camlについて 1.1.1��ML・Objective Caml の特徴 1.2��参考書，資料，マニュアル 1.3��環境設定 Chapter�2�� 2.1��インタラクティブコンパイラを使う 2.1.1��簡単な使い方 2.1.2��その他: ファイルからのプログラムの読み込み・コメント 2.2��基本データ型とその演算 2.2.1��unit型 2.2.2��int型 2.2.3��float型 2.2.4��char型 2.2.5��string型 2
Objective Caml 入門五十嵐 淳 京都大学 工学部情報学科計算機科学コース 大学院情報学研究科知能情報学専攻 e-mail: igarashi@kuis.kyoto-u.ac.jp September�24, 2007
このページを最初にブックマークしてみませんか？
『www.sato.kuis.kyoto-u.ac.jp』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
