2020年のEgisonの進捗

去年の12月のAdvent Calendarで、開発中であったEgisonの新しい構文についての記事を書いたのですが、その後の進展などを書いてなかったので書きたいと思います。 また年末が近いので、その他の開発の進捗についても話したいと思います。 構文について 先の…

2019年の総括

1-3月 CPU実験をしつつ将来の進路で結構悶々としていた。あまりいい思い出がない この頃にようやくHaskellにちゃんと入門した 4-6月 4Sセメスターは結構授業を取る必要があって忙しかった。演習3はテーマが合わなくて迷走し続けていた今井研以外はそれなりに…

Haskellライクな構文をEgisonに実装している話

これは言語実装Advent Calendar 2019の2日目の記事です。 私は少し前から、楽天技術研究所でEgisonの開発アルバイトをしています。入社してから初めての大きなプロジェクトとしてEgisonの構文を新しくするというのを担当しているので、その紹介と、設計/実装…

セキュキャン2019 参加記 (データベースゼミ)

8/13〜17に行われていたセキュリティ・キャンプ全国大会で、集中開発コースのX-III データベースゼミに参加してきました*1。 事前学習からキャンプ期間中を通して経験したさまざまなことを、時系列順に振り返っていこうと思います。 事前学習 講師の方から講…

Coqで「停止性 + 弱合流性 = 合流性」の証明

Coq

小ネタです。 Abstract Rewriting Systemにおいて、「停止性と弱合流性(局所合流性)を持つ書き換え系は合流性を持つ」という定理があります*1。 この証明は、書き換え系の停止性から整礎帰納法を使って示すのが一般的です。 整礎帰納法はCoqでどうやるんだろ…

自分の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 STEPとはGoogle Sum…