yamarten

Livelits: Filling Typed Holes with Live GUIs

Table of Contents

• 研究概要
  • やったこと

研究概要

やったこと

以下の2つの研究を1つに合体した

• GUIで値を入力できるプログラミング環境

yamarten

(* Coqでアドホック多相 *)
(* Coqで多引数の型クラスを用いた多相関数のサンプル *)
(* 型クラスに性質(定理)が書けるのもCoqらしさではあるが、その辺は他所でも紹介されているので割愛 *)
(* そういった機能については例えば: http://yosh.hateblo.jp/entry/20090904/p1 *)

(* 角括弧でのリスト記法が使いたかっただけなので、コンストラクタ直書きならImport不要 *)
Require Import List.
Import List.ListNotations.

(* 型クラス定義 ここでは関数を一つ持っているだけなので単に多相関数定義と思ってもいい *)

yamarten

論文紹介『Gradual Program Verification』

Table of Contents

• 概要

概要

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

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

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

---

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

yamarten

ホモトピー型理論(HoTT)に入門するために

前置き

HoTTに興味があるCS系の学生が、HoTT本の冒頭を読んだ体験を元に、知っておくと学び易くなりそうな話をまとめてみた。

対象は自分と同じ、型理論は少し知ってる^[1]けどホモトピーとかわからんという人。「型理論は知らんけどホモトピー論と圏論の用語はわかる」という人はそのまま本読めばいいと思うし、両方ともわからない人は学ぶモチベーションがよくわからない(し、とりあえずどちらかを学んだ方がいいと思う)のでとりあえず無視する。

HoTTについてはさわり程度の知識しかないまま書かれているため、話半分に読んでもらった方がいいと思う。

---

1. 「依存型に触ったことある」もしくは「TaPLを部分的にでも読んだ」あたりが基準になるだろうか。

yamarten

Table of Contents

• ライブラリ

目についたCoqのライブラリ/プラグイン/開発環境などの覚え書き

実用面は気にせず、研究用や無メンテも載せる

ライブラリ

Coqソースファイルのみで構成されるもの

yamarten

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

Table of Contents

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

おことわり

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

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

自分について

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

Semantic-Based Program Verifiers for All Languages

前置き

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

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

yamarten

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

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

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

yamarten

The Incredible Proof Machine

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

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

とりあえずゲーム

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