会社を作って最初にやったことその2 銀行口座開設チャレンジ

法人の銀行口座開設は難しいと聞いていましたが、実際どんどん厳しくなっているようです。 取引先からの入金にも役員報酬(自分への給料)の支払いにも社会保険の支払いにもクレジットカード作成にも法人の銀行口座がないと不便ですので最優先で法人口座開設を…

会社を作って最初にやったことその1 謄本の取得など

会社が設立(登記申請)してからやることはたくさんあるようです。私がやったことを時系列順に列挙します。 ** やったこと *** 銀行口座開設のWeb申請 手数料の安いジャパンネット銀行をマネーフォワード経由で申請しました。謄本がなくてもできますが設立(予…

会社を作りました

株式会社proof ninjaという会社を作りました。*1 株式会社proof ninja 今日からはこの会社の代表になります。OCamlの達人として名高いcamlspotterさんの ダイラムダ株式会社 から仕事をもらいます。ブロックチェーンプロトコルTezosを証明して世界一安全な暗…

会社を作ります その2

前回までのあらすじyosh.hateblo.jp あれからさらにやったこと 定款認証 マネーフォワード会社設立 で定款を作成すると提携の行政書士の先生が対応してくださいます。私の場合は行政書士法人TOTALという事務所の先生に丁寧に対応してもらいました。これらを…

会社を作ります その1

会社を作ろうとしています。ウェブ上にも身の回りでもあまり情報がまだ少ないと感じているため、このような記事が今後起業する誰かの参考になるかもしれません。 概要 会社名: 株式会社 proof ninja 事業内容: ソフトウェアの開発・検証 設立希望時期: 今年…

Tezosに参加しました

7月からDaiLambda社さんのお手伝いとして暗号通貨Tezosの仕事をしています。 Tezosとは TezosはOCamlとCoqを使って開発されているブロックチェーンプロトコルであり、暗号通貨の名前でもあります。スマートコントラクト言語 Michelson が静的型付き言語であ…

Coqで命題論理の標準形

この記事はTppMark11の問題をCoqでやってみたという内容である。問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Ter…

依存関係のある値のうちの一部をrewriteしようとしたときの問題

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表…

OCamlとCoqを連携してIO処理をモナディックに扱う

この記事は OCaml Advent Calendar の5日目の記事です。OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。 http://github.com/yoshihiro503/coqioこのライブラリを使えば、例えば次のようなコードを書くことができる。 Require I…

証明された証明支援器をScalaで書いてみた

この記事はTheorem Proving Advent Calendarの7日目の記事である。静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが…

VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。

VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初め…

fold_leftとfold_rightが同じになるとき

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。 Definition xs := …

tmiyaさんの練習問題をラムダ式で解いてみた

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。このような…

CPS変換されたフィボナッチ関数の証明をしてみた

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。http://ideone.com/3CQOnしかしfib_cps関数をもっと美しく定義できないものだろうか。[…

Coqプログラマの集会、Coq庵でした

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。スライドは以下から参照できます。 Coq庵 - coqグループ

OCamlでlet recを使わずにfact関数を定義する

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

TDDBC名古屋に行ってきました。

TDD Boot Camp名古屋に参加しました。id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。 当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇…

Alloyセミナーに行ってきました

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記TDDBC名古屋で2日間テスト駆動開発を行った直後で…

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676まずは集合AとA上の掛け算とサクセ…

Coqで多変数多項式の簡約

変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary opera…

第3回 Formal Methods勉強会に行ってきました。

第3回FormalMethods勉強会 : ATND (via fm-forum @ ウィキ - トップページ) 場所は喫茶ルノアールというところの中にある会議室でした。 前半Alloyの話をid:kencobaさんが、後半はCoqの話をtmiyaさんがするという形式でした。13時から19時まで6時間でしたが…

OCamlerのためのCoq便利モジュールを公開してみた

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

迷路の試験問題を解いてみた

Coq

参考:人材獲得作戦・4 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る…

Coqで多重再帰のデータ構造を証明する

Coqでは一重の再帰的なデータは例えば次の様に定義できる。 Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A). Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。 list_in…

Getting Started with Agda アグダを始めよう

Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。OSのディストリビューションは最近リリースされた Ubuntu 9.10。 非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。 Agdaのインストール Agdaの標準…

直観主義論理での二重否定除去と排中律の同値性

同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。 Lemma p10_left : (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)). Proof. intros. apply H. intro. elim (H0 H2). apply H1. Qed. …

1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。 Proposition p09 : forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C. Proo…

あるソート関数がちゃんとソートする事を証明

以前Merge Sort を実装して証明した。 http://d.hatena.ne.jp/yoshihiro503/20090923ソースコード全体は以下。 http://bitbucket.org/yoshihiro503/mergesort/

reverse (reverse list) == listとなる事を示す

http://d.hatena.ne.jp/yoshihiro503/20090708 で証明した。

リストの結合関数 ++ の結合則 l1 ++ (l2 ++ l3) == (l1 ++ l2) ++ l3

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。 Require Import List. Proposition p06 : forall {A} (l1 l2 l3:…