Skip to content

Instantly share code, notes, and snippets.

View yoshihiro503's full-sized avatar

YOSHIHIRO Imai yoshihiro503

94 followers · 48 following
View GitHub Profile
@yoshihiro503
yoshihiro503 / 業績目録2026.md
Created December 11, 2025 09:59

著書

  • 型システム入門 −プログラミング言語と型の理論, オーム社 (2013/3/26)
  • 入門OCaml ~プログラミング基礎と実践理解, 毎日コミュニケーションズ (2007/5/22)

学術論文

  • システム群のBASE特性を保証するためのCoqを用いた検証 - 2013 Fundamental of Software Engineering.
  • 検証済みのコードによるCoqからScalaへのコード抽出 - 2014 The 31th Japan Society for Software Science and Technology Annual Conference

発表、講演

@yoshihiro503
yoshihiro503 / githubでforkの分岐点を探す.md
Created October 24, 2025 02:56

cometbft/cometbft から派生した 0xPolygon/cometbft リポジトリを見ているが、どのタイミングで分岐したか知りたい

分岐点のコミットを探す

git clone https://github.com/0xPolygon/cometbft.git cometbft-polygonfork
cd cometbft-polygonfork/
git remote add upstream https://github.com/cometbft/cometbft.git
git fetch upstream
@yoshihiro503
yoshihiro503 / Heimdall_checkpoint.go_fungraph.dot.md
Last active May 15, 2025 08:55

Alt text

#CUT
digraph G {
    aize ="4,4";
    subgraph cluster_public {
        label="Public";
        Start [shape=box];
        RegisterTasks [shape=box, layer=cluster_public];
        Stop [shape=box];
@yoshihiro503
yoshihiro503 / Coqのコードをopamに登録する方法.md
Last active April 11, 2025 07:56
@yoshihiro503
yoshihiro503 / CoqのModule内定義に関するglobがなんか変な件について.md
Created August 30, 2024 06:59

mathcomp analysisのtopology.vにおいて，

...
Module PropInFilter : PropInFilterSig.
  Definition t := prop_in_filter_proj.
  ...
End PropInFilter.
Notation prop_of := PropInFilter.t.
...
@yoshihiro503
yoshihiro503 / 長さ付きリストの証明_ssreflect.v
Created July 12, 2024 06:42
From mathcomp Require Import all_ssreflect.
Require Import JMeq.
Inductive sizseq (T:Type) : nat -> Type :=
| SizNil : sizseq T 0
| SizCons n : T -> sizseq T n -> sizseq T n.+1.
Lemma sizseq0nil_aux (T:Type) n : forall xs : sizseq T n, n = 0 -> JMeq xs (SizNil T).
Proof.
@yoshihiro503
yoshihiro503 / coqtokyo_EqClass_sort2.v
Last active April 30, 2024 11:47
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* :> を複数持つと予期せぬことがおきることがあるぞ *)
Structure S : Type := MakeS {
sort2 :> Type;
sort :> Type;
@yoshihiro503
yoshihiro503 / mathcompbook_edivn.v
Created March 20, 2024 00:05
From mathcomp Require Import all_ssreflect.
Fixpoint evivn_rec pred_d m q :=
if m - pred_d is m'.+1 then edivn_rec pred_d m' q.+1 else (q, m).
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
Lemma edivn_recP1 q r m pred_d q0:
(q, r) = edivn_rec pred_d m q0 ->
r < pred_d.+1.
@yoshihiro503
yoshihiro503 / 民間企業が京都大学教職員へ技術顧問として兼業依頼する方法.md
Last active February 21, 2024 03:41
@yoshihiro503
yoshihiro503 / DMM_Coq_School_Day4.v
Last active September 4, 2023 01:44
Require Import String List.
Import ListNotations.
Open Scope string_scope.
Definition aaa := 1+2.
Definition bbb := aaa * 5.
Definition foo x y:= 2*x + y.
Compute foo 1 2.