Table of Contents
- Interests
- Links
- Articles
- Publication
- Activities
- Work Experience
- Software and Hardware
- GPG Public Key
- Current status
Interests
- Executable and Linkable Format of Linux
- Linux kernel inside
- Program analysis
Links
Articles
- MN-Coreランタイム – MN-Coreを動かすソフトウェア (in Japanese) / MN-Core runtime – software which runs MN-Core
- ros3fs - オブジェクトストレージ用の高速な読み取り専用FUSEファイルシステム (in Japanese)
- Linux のローダを自作する (in Japanese) / Alternative Linux loader (in English)
- Linux におけるデバイスファイルの仕組み (in Japanese) / How device file in Linux works (in English)
- jendeley - JSON ベースの文書管理ソフトウェア (in Japanese) / jendeley - a JSON-based document organizing software (in English)
- Linux kernel をソースコードからビルド、インストールするシェルスクリプトを書いた (in Japanese)
- LD_AUDIT and Global Offset Table (in Japanese)
- What is GNU_IFUNC? (in Japanese)
- What and how does libc save information into jmp_buf used in setjmp and longjmp? (in Japanese)
- JAX から MN-Core を利用する (in Japanese)
- As the main mentor, I made the prototype of XLA to ONNX converter and support Maekawa-san during intern.
Publication
- Kernel/VM 探検隊@東京 No16
- Talk on sloader
- Slide: 自作ローダのための libc 初期化ハック
- Kernel/VM 探検隊 online part5
- Short talk on AT_RANDOM
- Slide: 補助ベクトルとプロセスのロード
- ICFP 2020 Haskell Implementation Workshop
- Sweet Egison: a Haskell Library for Non-Deterministic Pattern Matching
- APLAS 2019
- A Dependently Typed Multi-Stage Calculus – This is a formal multistage calculus with dependent types. We design its type system and prove type soundness.
- Paper on axiv
- Egison Workshop 2018
- Introduction to the type system of Egison.
- Handout of the type system
- Slide
- JSSST2018
- Type theory for multistage programming including dependent types
- Paper
- Private talk
- Random talk on glibc dynamic linker of Linux
- Slide: /lib64/ld-linux-x86-64.so.2
Activities
- The 11th Japan Olympiad in Informatics, Silver medal
- IPA The MITOH Project 2018
- Distibuted Search Engine Using Focus Crawling and Federated Search
Work Experience
- Software engineer, Japan, Preferred Networks, April 2020
- Internship, Japan, Rakuten Institute of Technology, March 2018 - April 2018
Software and Hardware
- ros3fs
- ros3fs, Read Only S3 File System, is a Linux FUSE adapter for AWS S3 and S3 compatible object storage such as Apache Ozone. ros3fs focuses on speed, only speed.
- sloader
sloaderis an ELF loader that aims to replaceld-linux.so.2ofglibc.- Introduction article (in Japanese)
- Introduction article (in English)
- jendeley
- jendeley is a JSON based document organizing software.
- Document
- Introduction article (in Japanese)
- Introduction slides (in Japanese)
- z3shape
- z3shape infer shapes in ONNX file using Z3 SMT solver.
- sold
- sold is a linker software which links depending shared objects to a binary or a shared object.
- Presentation in kernelvm (in Japanese)
- Demo
- kearch
- kearch is a distributed search engine made from scratch. There are two type of search engine – specialized and meta. A meta search engine takes query from uses and distribute it to appropriate specialized search engine.
- Final presenation of MITOU project (in Japanese)
- Demo movie in the final presenation (in Japanese)
- typed-egison
- typed-egison is a type checker for Egison programming language. I designed all typing rules for Egison and make type inferencer for Egison with Haskell. You can use it from interpreter.
- Repository
- wavplayer
- wavplayer is a mini music player using ATMEGA168 and SD card. I wrote FAT16 file system for ATMEGA168. Musics are stored in wav files in the root directory.
- cropass
- cropass is a password manager written in Go. I wrote this to use myself. You can generate, add and lookup password records.
- hinvader
- hinvader is a simple invader like game wirtten in Haskell. I used GLUT to reder the screen.
- ml2wasm
- ml2wasm is a compiler from ML like language (MinCaml) to WebAssembly.
- N-body-simulation
- N-body-simulation is a toy n-body simulator.
GPG Public Key
- Fingure print: 3FB4269CA58D57F0326C1F7488737135568C1AC5
- Public key file