yamarten

Table of Contents

• ライブラリ

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

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

ライブラリ

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

yamarten

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

前置き

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

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

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

---

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

yamarten

論文紹介『Gradual Program Verification』

Table of Contents

• 概要

概要

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

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

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

---

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

yamarten

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

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

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

yamarten

Livelits: Filling Typed Holes with Live GUIs

Table of Contents

• 研究概要
  • やったこと

研究概要

やったこと

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

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

yamarten

/*
firequix.jxa
bookmarklet organizer for Firefox with BetterTouchTool inspired by quixapp.com
*/

'use strict'

function run(argv) {
  // Please create bookmark to "javascript:%s" and set keyword.
  const keyword = 'javascript'

yamarten

// ==UserScript==
// @name        YouTube DateTime
// @match       https://www.youtube.com/watch*
// @grant       none
// @version     1.0.0
// @description     Replace info with absolute datetime
// @description:ja  YouTubeの動画投稿・配信開始日時を表示
// ==/UserScript==

(() => {

yamarten

11/13時点のドキュメント準拠

実装はあんまり見ずに、ATPの雰囲気を把握するためのメモ

概観

要素としては以下のような感覚。

• Repository: 署名つきRDB
• データ構造がRDB(というか表)という話で、SQL-likeな操作が規定されてるわけではない

yamarten

atprotoの署名は何を保証するか

atprotoではrepositoryに対して署名を行うが、これによって何が嬉しいのかを考える。

【結論】 大事なrecordを提示する時は署名も示す文化が根付けばメリットはあるが、周知されなければ署名し損 ^[1]

おさらい

とりあえず以下の2つの仮定をおく。これはかなり強い仮定なのでその影響は別途検討する必要がある。

---

1. 当然のことを言っているだけのような気もする……

yamarten

ATP用語

用語	別名	意味	出典	備考