yoshihiro503’s gists

yoshihiro503 / TaskMonad.cs

Created November 20, 2012 07:39 — forked from bleis-tift/TaskMonad.cs

C# で非同期タスクモナド書いてみた。

	using System;
	using System.Collections.Generic;
	using System.Linq;
	using System.Text;
	using System.Threading;
	using System.Threading.Tasks;

	namespace Proofcafe
	{
	public static class TaskMonad

yoshihiro503 / TaskMonad.cs

Created November 20, 2012 07:45 — forked from bleis-tift/TaskMonad.cs

C# で非同期タスクモナド書いてみた。

	using System;
	using System.Collections.Generic;
	using System.Linq;
	using System.Text;
	using System.Threading;
	using System.Threading.Tasks;

	namespace Proofcafe
	{
	public static class TaskMonad

yoshihiro503 / trans_pukiwiki_fnames.ml

Created December 10, 2012 07:27

pukiwikiのwikiデータのファイル名を読みやすい構造に変換する ref: http://qiita.com/items/25d3ac45603ae1090254

	(*
	pukiwikiの内部データのファイル名を可読できる名前に変換する
	ls /PUKIWIKIDIR/wiki/*.txt \| ocaml trans_pukiwiki_fnames.ml
	*)
	let outdir = "out/"
	let verbose = true

	let (\|>) x f = f x
	let (@@) f x = f x
	let (!%) = Printf.sprintf

yoshihiro503 / Repeats.v

Created January 26, 2013 06:41

#proofcafe

	Inductive repeats {X:Type} : list X -> Prop :=
	\| RP_hd : forall x xs, appears_in x xs -> repeats (x::xs)
	\| RP_tl : forall x xs, repeats xs -> repeats (x :: xs)
	.

yoshihiro503 / GetBytes.scala

Last active December 12, 2015 07:38

Scala でバイナリを読んで、Iterator[Byte]を得る方法ってどうやるのが一番いいのだろうか？

yoshihiro503 / mumumu.ml

Last active December 14, 2015 02:19

ocaml-4.00.1 および ocaml-3.12.1で確認。バイトコードでもネイティブでも起きる。 -vmthreadだと起きない $ ocamlc -thread unix.cma threads.cma mumumus.ml

	(*
	(なぜかこの関数定義があると下記でSIGALRMが呼ばれなくなる )
	let hogehoge f x = Thread.create f x
	*)

	let wait () =
	let m = Mutex.create () in
	Mutex.lock m;
	let c = Condition.create () in
	Condition.wait c m

yoshihiro503 / le_Sn_n.v

Created February 23, 2013 07:31

「ソフトウェアの基礎」 Rel_Jの練習問題 le_Sn_n の形式的な証明 http://proofcafe.org/sf/Rel_J.html

yoshihiro503 / rsc_trans.v

Created February 23, 2013 08:21

「ソフトウェアの基礎」Rel_J 練習問題 rsc_trans の証明

	( ** 練習問題:★★, optional(rsc_trans) *)
	Theorem rsc_trans :
	forall (X:Type) (R: relation X) (x y z : X),
	refl_step_closure R x y ->
	refl_step_closure R y z ->
	refl_step_closure R x z.
	Proof.
	intros. induction H.
	apply H0.

yoshihiro503 / rtc_rsc_coincide.v

Created February 23, 2013 08:24

「ソフトウェアの基礎」Rel_J 練習問題 rtc_rsc_coincide の証明

	( ** 練習問題:★★★, optional (rtc_rsc_coincide) *)
	Theorem rtc_rsc_coincide :
	forall (X:Type) (R: relation X) (x y : X),
	clos_refl_trans R x y <-> refl_step_closure R x y.
	Proof.
	intros. split; intro H.
	induction H.
	apply rsc_R.

	apply H.

yoshihiro503 / sf_imp_optimize_0plus_b.v

Created April 27, 2013 07:11

ソフトウェアの基礎 Imp_J.v 練習問題

	(* **** Exercise: 3 stars (optimize_0plus_b) *)
	( ** 練習問題: ★★★ (optimize_0plus_b) *)
	(* Since the [optimize_0plus] tranformation doesn't change the value
	of [aexp]s, we should be able to apply it to all the [aexp]s that
	appear in a [bexp] without changing the [bexp]'s value. Write a
	function which performs that transformation on [bexp]s, and prove
	it is sound. Use the tacticals we've just seen to make the proof
	as elegant as possible. *)
	(** [optimize_0plus]の変換が[aexp]の値を変えないことから、
	[bexp]の値を変えずに、[bexp]に現れる[aexp]をすべて変換するために

YOSHIHIRO Imai yoshihiro503