【新機能】作り忘れたまとめはありませんか?31日前まで期間指定してまとめが作れる高度な検索ができました。有料APIだからツイートの漏れはありません!

#ATS2 の作者Hongwei Xiの研究室に行ってきたよ

#ATS2 の作者Hongwei Xiの研究室に行ってきたよ
ネタ
1561view 1コメント
2
ログインして広告を非表示にする
Q @masterq_mogumog 2015-08-30 00:47:47
ちょっと時間があるからHongweiのコメントでもまとめよう。
Q @masterq_mogumog 2015-08-30 00:49:38
Xanaduは悪いアイデアだったのか?」「DML=>Xanadu=>ATSのようにコンパイラは成長した。Xanaduで採用したC言語文法は型表現に対して柔軟ではなかった」C言語文法の方がユーザフレンドリだけどしょうがないのかな cs.bu.edu/~hwxi/Xanadu/X…
Q @masterq_mogumog 2015-08-30 00:52:04
「読むべきソースコードのリストはあるか」「今はセッション型のコードがおすすめ。現状はErlangバックエンドに対する実装がある。C言語でも相当のC言語コードサポートを書けば使えるはず」 github.com/githwxi/ATS-Po…
Q @masterq_mogumog 2015-08-30 00:54:34
「セッション型の実装ではボイラープレート対策のために #codegen2 という新しいキーワードを使っている。これはHaskellのderiveのようなことができるが、テンプレートを使っているためその挙動を細かくユーザが調整できる」 github.com/githwxi/ATS-Po…
Q @masterq_mogumog 2015-08-30 00:56:04
「コーディングスタイルはどうしてあんななの?型シグニチャの宣言はあれでいいけど、インデントはつけてよ。日本のユーザにはフォーマッタ作る動きさえあるよ」「フォーマッタ作るのはいいね!」はぐらかされた。
Q @masterq_mogumog 2015-08-30 00:57:30
「将来的にC言語側でのエラーをATS側のエラーに持ち上げることは可能なのか。今のC言語側でのエラーはわかりずらい」「C言語側でのエラーをATS1のようにもっとわかりやすくすることは可能だと思う」
Q @masterq_mogumog 2015-08-30 00:59:15
「丁度良い証明コード量とは?多すぎると証明が大変。少ないとコードが危険」「Z3を使った自動証明が可能になるケースはあると思う。ただし、証明できなかったときに型エラーから判別するのは困難になるだろう」つまり半自動の証明作ってもパラダイスがひろがってる訳じゃないってことですね。。。
Q @masterq_mogumog 2015-08-30 01:01:30
「ATS1時代の思い出ある? ATSfloat scg.ece.ucsb.edu/ats.html とかあったけどあのユーザ層はどこいっちゃったの?」「ATSfloatは僕とは別に開発していた。最近はコンタクトがないね」やっぱりATS1=>ATS2の移行でかなりのユーザが消えたのでは
Q @masterq_mogumog 2015-08-30 01:02:16
「ATSに関する論文を出すならFlopsも良いのではないか。日本で開催するし」
Q @masterq_mogumog 2015-08-30 01:04:53
William Blairから。「Habitっていう組込Haskell実装があるよ hasp.cs.pdx.edu 」「ぼくの古いAVRなどの記事は blogs.bu.edu/wdblair/ から読めるよ」
Q @masterq_mogumog 2015-08-30 01:06:20
「セッション型は多数のホスト間でのプロトコルやメニーコア上のコードなどに有効。最近はAmazonがお金を出して研究している。君も parallella.org とかで #ATS2 のセッション型を使ったアプリケーション作ってみるのもいいんじゃない?」
Q @masterq_mogumog 2015-08-30 01:09:54
「ボストン大学でドイツの組み込みOS規格にのっとったOSを作っていて、その上で動くアプリケーションを #ATS2 で書くこころみをやってみたことがある。この時はOS実装そのものはC言語で書いた」
Q @masterq_mogumog 2015-08-30 01:11:05
証明コードを書くときは、あまり束縛名を上書きしない方が良い。型エラーがどの束縛に対するものなのかわかりにくくなる。」
Q @masterq_mogumog 2015-08-30 01:14:37
ミーハーだけど写真取った。左から Steinway Wu, Hongwei Xi, 僕, William Blair pic.twitter.com/TpWA3jaGgW
 拡大
Q @masterq_mogumog 2015-08-30 01:15:53
Hongweiの研究室に行くには、この地図にしたがって歩いて、、、 pic.twitter.com/URY8KmJvHz
 拡大
Q @masterq_mogumog 2015-09-28 21:47:07
ボストン大学でATS言語アプリケーションを作った際のドイツの組み込みOS規格のRTOSはOSEKだった。思い出した。 / OSEK - Wikipedia, the free encyclopedia en.wikipedia.org/wiki/OSEK

ブックマークしたタグ

あなたの好きなタグをブックマークしておこう!話題のまとめを見逃さなくなります。

コメント

Q @masterq_mogumog 2015-09-28 21:47:32
まとめを更新しました。
ログインして広告を非表示にする
ログインして広告を非表示にする