yamarten

Atom のススメ

エディタの方。個人的結論としては「かなり良いけど乗り換えるならもう少し（1.0くらいまで）待ってからでもいいんじゃないか」という感じになると思う。

公式ドキュメントが整備された記念にgistの試し書きも兼ねて書きなぐり。ちなみにこれ自体もAtom で Gist It とか Asciidoc Preview とか使って書いてる。
比較対象は Sublime Text 。 Brackets は特化型っぽいし Light Table はまだ実用的に感じない（Eve 含め少し気になってはいる）。宗教系はもう必要時以外は触れたくない。

気に入ってるところ

• 拡張性

yamarten

ぼくがかんがえたさいきょうのぶっくまーくれっと

次のページに進むだけなんだけど、 BTT に登録して毎日使ってる程度には便利なのでどこかに残しておきたかった。具体的には番号を進めるやつとhttp://hooki.blog23.fc2.com/blog-entry-43.htmlを組み合わせただけなので何か作ったわけではない。

次のページ

javascript:(function()%7Bvar%20xs=document.evaluate(%22//link%5B@rel='next'%20or%20@rel='NEXT'%5D/@href|//a%5B@rel='next'%20or%20@rel='NEXT'%5D/@href%22,document,null,XPathResult.FIRST_ORDERED_NODE_TYPE,null);if(xs.singleNodeValue)location.href=xs.singleNodeValue.textContent;else%20if(document.location.href.match(/%5E(.*?)(%5Cd+)(%5B%5E%5Cd%5D*)$/))%7Bvar%20r=RegExp.$2-0+1;for(;(''+r).length%20%3C%20RegExp.$2.length;)%7Br='0'+r;%7Ddocument.location=RegExp.$1+r+RegExp.$3;%7D%7D)();

yamarten

(Macで)どこでもAtom

ブラウザのテキストボックスやtwitterクライアントのツイート入力をAtomに任せられるようにしてみた。

経緯

wikiとか書くときにエディタ使いたかった。Atom使うかどうかはともかく。

ここに外部アプリのテキストをエディタで編集する方法がまとまってたけど、どれも惜しい。WinのTextEditorAnywhereみたいな汎用的で無料のものがMacにもほしい。

yamarten

The Incredible Proof Machine

この投稿は今年読んだ一番好きな論文_アドベントカレンダー2016の 1 日目の記事です。

昨晩、もう 12 月も始まるからと Adventar 漁って RSS 登録していたら、このカレンダーを見つけてしまった。せっかく素晴らしい企画なのに初日から無人なんてもったいない（そしてあわよくば賞品欲しい）、ということで駆け込み一番槍をいただいた。

とりあえずゲーム

なにはともあれ、まずはこのサイトを紹介したい。

yamarten

研究室で ProofScript について紹介したが、せっかく面白い言語なので共有。

ps1.pdf が大元のプロジェクトである ProofPeer の紹介と ProofScript のプログラミング言語部分の紹介。 ps2.pdf が ProofScript の残りの紹介。

正確性とかについては保証できないので自分で確かめていただきたく。

yamarten

基本的に日本語資料しか読まない人からの意見なので知識不足ではあると思われる。反論とかツッコミとか歓迎。

• 音声主体

  • 言文一致のせいで記号とか使いにくい

    • 特定パターンに該当する場合のみ特殊記法でそれ以外は音通り、でいいのかもしれない

    • はじロジでは「音素と文字が一対一」らしいけどソースが知りたい

  • どんな文字を使ってもいい？

    • 現状ネット利用が一般的に見えるのに文字定めないのはどうなの

    • そもそも CLL だと普通にローマ字を使う感じなのでこれもソースが気になる

• ドキュメント

yamarten

(* for 8.6 *)
(* based on https://gist.github.com/keigoi/c3817d2aad09e9179465d4261cf5ef9b *)
(* "using"縛り *)

Require Import PeanoNat.

Fixpoint sum (n:nat) : nat :=
  match n with
  | O => O
  | S n => S n + sum n

yamarten

今年読んだ論文2017アドベントカレンダーの補足

Table of Contents

• おことわり
• 自分について

おことわり

あれから5ヶ月が過ぎました。年も年度も変わり、いただいたビールも無くなり、修了して社会人になり、今更どころではないですが、一応あの記事についてもう少しだけ書いておこうと思います。

9割方独り言というか覚書のつもりで書いているので、蛇足が過ぎて百足の如き様相を呈していますが、ご了承ください。

自分について

yamarten

Semantic-Based Program Verifiers for All Languages

前置き

このgistは今年読んだ一番好きな論文2017 Advent Calendarの1日目の記事です。

去年、覚え書きのような記事で参戦したら、歓迎の言葉に加えて参加賞まで貰ってしまった者です。あれで終わらせるのは申し訳ない以前に悔しいので、今回はよそゆきの文章でガッツリ書いてリベンジすることで感謝の言葉に替えたいと思います。

yamarten

論文紹介『Gradual Program Verification』

Table of Contents

• 概要

概要

• 利用者の手間のかけ具合に応じて2種類のプログラム検証^[1]手法を混合して使う『漸進的検証』を提唱

• 既存の静的検証手法から漸進的検証手法を構成する枠組みを考案

• C風のプログラミング言語に対する漸進的検証手法を実際に構成

---

1. ここではverificationの訳語です。certificationとの使い分け(用法/訳語共に)を誰か教えてほしい。