めたせぴ2015☆ゆく年くる年 草稿
-
masterq_mogumog
- 1115
- 1
- 0
- 1
-
- いいね！1
I moved to Mastodon.
@masterq_mogumog
あと、最近はJVeriFast-UGを作らねばならない気運があるんだけど、たぶんそれは僕がいなくても誰かやってくれそうらしいので、来年は #VeriFast のサーベイにも力を入れたい。
2015-12-30 19:26:50
I moved to Mastodon.
@masterq_mogumog
静的な関数に本体も書けて、それをSMTソルバで解く、というのがZ3の存在下におけるまっとうな言語なんだと思う。不幸にも証明関数にしか本体を書けず、そして証明関数は自動で推論されない。。。 #ATS2
2015-12-30 19:31:31
I moved to Mastodon.
@masterq_mogumog
だから、、、だから、、、Applied Type Systemを持つ別の言語を作るのには現在では意味があるんだよ！
2015-12-30 19:32:09
I moved to Mastodon.
@masterq_mogumog
Hongweiちゃんは今日も元気だなぁ / githwxi (Hongwei Xi) github.com/githwxi
2015-12-30 19:35:05
I moved to Mastodon.
@masterq_mogumog
今年1月には “ATS Programming Foundations” jats-ug.metasepi.org/doc/ATS2/ATS_F… という教科書を書こうと思いたったようだ。まったく今でも未完成だけれど、この形式の入門が今のATSコミュニティにないという意見は今も変わっていない。
2015-12-30 19:41:32
I moved to Mastodon.
@masterq_mogumog
ATS Programming Functationsの執筆は今年9月で途切れている。がんばれ自分。
2015-12-30 19:42:17
I moved to Mastodon.
@masterq_mogumog
合計12回のプレゼンを行なった。昨年は14回プレゼンをしたので、まぁあまりペースはかわらなかったと思っていいのかもしれない。 github.com/master-q/maste…
2015-12-30 19:46:25
I moved to Mastodon.
@masterq_mogumog
プレゼンの中で2つ選ぶとしたら1つ目は ATS/LF for Coq users slideshare.net/master_q/atslf… だろうと思う。おそらくはじめて解りやすく #ATS2 における定理証明について説明した文書だと思っている。この資料を書けるようになるのに半年かかった
2015-12-30 19:49:10
I moved to Mastodon.
@masterq_mogumog
もう1つの注目すべきプレゼン資料は Static typing and proof in ATS language slideshare.net/master_q/stati… だと思う。これまでなにげなく使っていたATSの静的な部分について非常に稚拙だけれど解説しているつもりです。。。
2015-12-30 19:50:29
I moved to Mastodon.
@masterq_mogumog
これで、ようやっとATSの #動的な部分 #静的な部分 #証明の部分 について理解することが僕の中でできるようになったのでした。
2015-12-30 19:51:07
I moved to Mastodon.
@masterq_mogumog
そうそう。PPLでもATSを紹介したのでした。 / ATS Programming Tutorial at PPL 2015 - Metasepi metasepi.org/en/posts/2015-…
2015-12-30 19:54:13
I moved to Mastodon.
@masterq_mogumog
PPLは、、、どうなんだろうか。発表してもお金にならなそう、という点はなんとなくわかったので、後はどうするかなのですが。。。。
2015-12-30 19:54:48
I moved to Mastodon.
@masterq_mogumog
もっとブログは書かないといけないなぁ / Home - Metasepi metasepi.org
2015-12-30 19:56:08
I moved to Mastodon.
@masterq_mogumog
大きな文書を作るよりもブログエントリを束ねて教科書とする方が、現代的で現実的なのかもしれない。。。
2015-12-30 19:56:47
I moved to Mastodon.
@masterq_mogumog
4月5月には「Arduinoをはじめよう」本 amazon.co.jp/Arduino%E3%82%… の例題をATS化すべく試していた。後に"Arduino programing of ML-style in ATS"論文を書くベースになる metasepi.org/papers.html
2015-12-30 20:06:56
I moved to Mastodon.
@masterq_mogumog
5/2にHongweiによる論文査読祭がはじまっている。正直、自分の文章なのに査読スピードについていけなくておちこぼれていた思い出がある。査読は5/5で終わっている。Hongweiちゃんさすが仕事はやいな。。。
2015-12-30 20:09:37
I moved to Mastodon.
@masterq_mogumog
5/5ぐらいにRust組み込みについて少し調べたようだ。C言語との界面でunsafeの嵐になるのと、ランタイム抜きのRustビルド手順が安定していなかったのでそれ以上は調べていません / Embedded Rust and more slideshare.net/master_q/embed…
2015-12-30 20:13:22
I moved to Mastodon.
@masterq_mogumog
5/14に「ソフトウェアの基礎 Prop_J: 命題と根拠」 proofcafe.org/sf-beta/Prop_J… を #ATS2 で書き直してみようと思いついたらしい。これが暗く長い今も抜け出せない闇への入口だった。。。 / github.com/jats-ug/practi…
2015-12-30 20:17:44
I moved to Mastodon.
@masterq_mogumog
さんざHongweiに質問した気がするけどatslf_dayは1ヶ月で書きおわって、回文ライブラリを5/29に作りはじめて6/19に完成している。これが後にプレゼン資料と同人誌になった slideshare.net/master_q/atslf… paraiso-lang.org/ikmsm/books/c8…
2015-12-30 20:25:33
I moved to Mastodon.
@masterq_mogumog
6/25-6/30まではC言語側から多段のポインタがATSに投げつけられたときに、どう型をつければ妥当なのか試していたみたい。今ならもっと良い案を思いつきそう / github.com/jats-ug/practi… github.com/jats-ug/practi…
2015-12-30 20:28:56
I moved to Mastodon.
@masterq_mogumog
7/12に不幸にも「マージソートを線形型で証明的に書く」ことを思いついてしまう。この格闘は9/25に絶望のコミットメッセージを残して終わっている。/ github.com/jats-ug/practi…
2015-12-30 20:32:43
I moved to Mastodon.
@masterq_mogumog
「証明的な線形マージソート」の鍵となるアイデアは「インプレースマージソートなら、線形で書き下すことができ、かつある程度の証明も与えられるだろう」というものだった / in-place merge sort - 鍋あり谷あり d.hatena.ne.jp/Nabetani/20071…
2015-12-30 20:34:00