自分のCoq環境 (with Vim)

Coq

一年前くらいにCoqを触り始めて、Software FoundationやCPDTなどを読みながら細々とCoqの勉強を続けています。 Coqを使うための環境としては、CoqIDEやProofGeneralなどが有名ですが、 前者はUIが充実していなくて使いにくく、後者はEmacsなので普段Vimを使…

情報系初心者の頃に使っていた教材などを振り返る

最近友人数人でグループを組んで、情報科学分野に女子を増やすためのアウトリーチ活動みたいなものをやろうとしています。 そのときに、自分が実際にプログラミング初心者だった時にどんな本やネットの資料をみて勉強や情報収集をしていたかということを久し…

Outreachyに応募できなかった話

タイトルに書いたようなことが最近起こってちょっと悲しかったのと色々考えさせられた気がするので備忘録がてら書き起こしてみます。 Outreachyとは? www.outreachy.org Outreachyとは、FOSS(Free Open Source Software)の開発者コミュニティにおける多様性…

Chromeでのインターン生活を振り返る

今年の夏にGoogle JapanのChrome(ブラウザ)チームで2ヶ月間インターンをしました。去年の夏も行ったので今年で2回目です。 今年のインターンはどんな感じだったのか、年末なので(?)ゆるく振り返ってみようかと思います。 インターンが決まった経緯 私は去年…

Software Foundation vol.1を読んだ

Coqやソフトウェア検証の入門書として知られるSoftware Foundation(以下SF)シリーズのvol.1,Logical Foundationを読むグループを学科で立ち上げて,3年生が始まる前の春休みに皆で読んでいた。3年生の前期が始まると忙しくて中断してしまったが,夏休みに入…

École Polytechniqueに行ってきた

2月の中旬頃から下旬頃にかけて2週間,パリのÉcole Polytechniqueでの研修に参加してきたため,振り返りを兼ねて滞在記を書こうと思います。 プログラムの説明 そもそもなんで行ってきたの? 私の所属する大学には体験活動プログラムというものがあり,学部…

2年Aセメスターの振り返り

情報科学科に入って最初のセメスターが終わりました。どんな授業を受けたのかなどを振り返ってみたくなったので記事を書いてみます。 授業 必修 計算機システム コンピューター・アーキテクチャを広く浅く網羅する感じの授業で,ALU,CPU,アセンブリ,OS,…

DFAの状態数最小化アルゴリズム

この記事はIS18er Advent Calendarの20日目の記事として書かれました。 別に大した話ではないのですが,アドベントカレンダーを埋めるために無理やり引っ張り出してきたネタです。 形式言語理論の授業で扱ったDFA(決定性有限オートマトン)の状態数最小化アル…

UNIX V6コードリーディング 備忘録

この記事はIS18er Advent Calendarの13日目の記事として書かれました。 最近学科でこの本を読むゼミをやっています。 はじめてのOSコードリーディング ~UNIX V6で学ぶカーネルのしくみ (Software Design plus)作者: 青柳隆宏出版社/メーカー: 技術評論社発売…

ENIACについて

この記事はIS18er Advent Calendar 2017の2日目の記事として書かれました。 先日大学の図書館でたまたまENIACについての本が目に入り,借りて読んでみたのですが,予想外に面白かったので, 今日はENIACの歴史とか技術的特徴について紹介する記事を書こうと…

Google STEP体験記

この記事は,情報系を勉強する女子大生 Advent Calendar 2017の2日目の記事として書かれました。 この記事では,私が2017年の6月頃から夏休みにかけて参加していたGoogle STEPについてご紹介したいと思います。 Google STEPとは? Google Summer Trainee Eng…

ブログ開設

東京で情報系の大学生をやっています。よろしくお願いします。