Skip to content

Instantly share code, notes, and snippets.

@yamarten
yamarten / livelits.asc
Last active Dec 1, 2019
livelits紹介
View livelits.asc

Livelits: Filling Typed Holes with Live GUIs

Table of Contents

研究概要

やったこと

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

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

@yamarten
yamarten / overload.v
Last active Mar 17, 2019
Coqでアドホック多相
View overload.v
(* Coqでアドホック多相 *)
(* Coqで多引数の型クラスを用いた多相関数のサンプル *)
(* 型クラスに性質(定理)が書けるのもCoqらしさではあるが、その辺は他所でも紹介されているので割愛 *)
(* そういった機能については例えば: http://yosh.hateblo.jp/entry/20090904/p1 *)
(* 角括弧でのリスト記法が使いたかっただけなので、コンストラクタ直書きならImport不要 *)
Require Import List.
Import List.ListNotations.
(* 型クラス定義 ここでは関数を一つ持っているだけなので単に多相関数定義と思ってもいい *)
@yamarten
yamarten / gradver.asc
Last active Jan 6, 2019
Gradual Program Verification
View gradver.asc

論文紹介『Gradual Program Verification』

Table of Contents

概要

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

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

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


1. ここではverificationの訳語です。certificationとの使い分け(用法/訳語共に)を誰か教えてほしい。
@yamarten
yamarten / hott_intro.asc
Last active Sep 16, 2018
HoTT本入門
View hott_intro.asc

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

前置き

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

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

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


1. 「依存型に触ったことある」もしくは「TaPLを部分的にでも読んだ」あたりが基準になるだろうか。
@yamarten
yamarten / coq_tools.asc
Last active Oct 18, 2020
Coq関連プログラムリンク集
View coq_tools.asc
Table of Contents

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

Coqのバージョン等はとりあえず気にしない

ライブラリ

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

View advent_omake.asc

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

おことわり

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

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

自分について

View sum.v
(* 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
yamarten / adventk.asc
Last active Dec 1, 2018
Kの紹介と検証器の話
View adventk.asc

Semantic-Based Program Verifiers for All Languages

前置き

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

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

@yamarten
yamarten / proofscript.asc
Last active Nov 10, 2017
ProofScript紹介
View proofscript.asc

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

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

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

You can’t perform that action at this time.