これまでに行った開発や情報発信について纏めています。

開発したもの

自作コンパイラ

GitHub - soukouki/10cc: C compiler training code based on https://www.sigbus.info/compilerbook

2024年の春から夏にかけて実装したC言語のコンパイラです。セルフホスト(自作したCコンパイラ自身で自分自身をコンパイルすること)に達成しました。途中までは自分1人で作り、途中からはセキュリティキャンプの[Cコンパイラゼミ2024]内で作業を行いました。

自作インタプリタ&勉強会

GitHub - soukouki/baby-interpreter: 学習用に作った、機能を拡張しやすいようなインタプリタです

2021年の夏ごろに実装し、秋ごろに勉強会を行ったJavaScript製のインタプリタです。このインタプリタを使い、同じサークルや友人などに対して勉強会を行いました。勉強会の内容としては、機能を制限したインタプリタを基に、参加者が各自で独自の方向性を持って言語を発展させるものでした。

この他にも自作言語のインタプリタの自作を2回ほど行っています。

Coqによるクイックソートの形式化

GitHub - soukouki/coq-quick_sort: Proving the quick sort with Coq.

クイックソートを定理証明支援系であるCoqによって形式化し、形式化したクイックソートが本当にソートできることを証明しました。

Coqによる集合論・群論の形式化

GitHub - soukouki/mathlib

松坂和夫「集合・位相入門」を元に、集合論の形式化を行いました。また、それ以外にも群論などの形式化を行いました。

Coq勉強会用の資料

GitHub - soukouki/coq-learning

友人にCoqを教える勉強会を開こうと思い立ち、「ならばの関係」という簡単なステップから、クイックソートの形式化までを行う勉強会の資料を作成しました。

OSSコントリビュート

Coqの標準ライブラリ

Briefly rewritten proofs of Finite_sets_facts.v by soukouki · Pull Request #17940 · coq/coq · GitHub

定理証明支援系であるCoqの標準ライブラリに対して、コード(証明)を簡単にするプルリクエストを送りました。

Ruby用DiscordBotライブラリ

fix Discordrb::Cache#server by soukouki · Pull Request #424 · discordrb/discordrb · GitHub

Fix Emoji#== by soukouki · Pull Request #590 · discordrb/discordrb · GitHub

Ruby用のDiscordのBotのライブラリである、discordrbに対してコントリビュートをしました。discordrbを用いてBotを制作している中でバグを発見し、それを修正する貢献をしました。

Simutrans

Vehicles show line name on otrp by soukouki · Pull Request #31 · teamhimeh/simutrans · GitHub

OSSで開発されているゲームであるSimutrans(正確には、そのforkであるOTRP版)に対して、機能追加を行うコントリビュートを行いました。

LT会活動

大学ではLT会を行うサークルに所属しており、これまで複数回発表してきました。スライドは下記のリンクから確認できます。

soukouki (@soukouki) on Speaker Deck

特に人気のあるスライドは以下のとおりです。

  • 自作Cコンパイラ 8時間の奮闘
    • セキュリティキャンプのCコンパイラゼミに参加した際に発生したバグについて話しました。
  • 次に流行る※プログラミング言語「Lean」
    • Leanという言語について、簡単な解説を行いました。

記事の執筆

はてなブログと、QuartzとGitHub Pagesによるブログによって情報発信を行っています。

はてなブログでは、数年前から記事を公開しています。詳しくはsoukouki’s diaryをご覧ください。

QuartzとGitHub Pagesによるブログについては、メモアプリObsidianからスムーズに記事を公開できるように自動化しています。詳しくはindexをご覧ください。