Skip to content

Instantly share code, notes, and snippets.

View yamarten's full-sized avatar

yamarten

4 followers · 1 following
View GitHub Profile
@yamarten
yamarten / yt_time.user.js
Created June 1, 2022 01:47
YouTubeの動画投稿・配信開始日時を表示
// ==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
yamarten / firequix.jxa
Last active August 11, 2020 05:56
MacのFirefox用ブックマークレットランチャ
/*
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
yamarten / livelits.asc
Last active December 1, 2019 12:59
livelits紹介

Livelits: Filling Typed Holes with Live GUIs

Table of Contents

研究概要

やったこと

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

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

@yamarten
yamarten / packages.asc
Last active September 20, 2019 01:44
Atomの各種機能

逆引きAtom

逆引きAtom

新世代のemacsを目指して作られた[1]エディタAtom。「emacsは環境」という言葉もあるように多機能なemacsに対し、Atomはどんな機能があるのかまとめてみた。「こんなこともできるよ」と「これオススメだよ」と「これよく探されるよ」がごっちゃになってるので、実用性はあんまり無い。特にエディタっぽい機能を求めている場合は他を参照のこと。

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

論文紹介『Gradual Program Verification』

Table of Contents

概要

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

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

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

1. ここではverificationの訳語です。certificationとの使い分け(用法/訳語共に)を誰か教えてほしい。
@yamarten
yamarten / adventk.asc
Last active December 1, 2018 13:08
Kの紹介と検証器の話

Semantic-Based Program Verifiers for All Languages

前置き

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

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

@yamarten
yamarten / advent_omake.asc
Created May 1, 2018 15:21

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

Table of Contents

おことわり

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

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

自分について

@yamarten
yamarten / sum.v
Last active February 26, 2018 04:49
(* 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 / ここが嫌だよロジバン.asc
Last active November 13, 2017 01:58
ロジバンに勝手に期待して裏切られた話

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

  • 音声主体

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

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

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

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

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

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

  • ドキュメント