お知らせ connpassではさらなる価値のあるデータを提供するため、2024年5月23日(木)を以ちましてイベントサーチAPIの無料での提供の廃止を決定いたしました。
料金・プラン等につきましては後日改めてご案内いたします。詳しくはこちらの お知らせをご覧ください。

お知らせ connpassをご利用いただく全ユーザーにおいて健全で円滑なイベントの開催や参加いただけるよう、イベント参加者向け・イベント管理者向けのガイドラインページを公開しました。内容をご理解の上、イベント内での違反行為に対応する参考としていただきますようお願いいたします。

このエントリーをはてなブックマークに追加

Feb

26

SF.lean勉強会

Coqで書かれたSoftware Foundations vol. 1をLean 4に翻訳します

Organizing : YAMAMOTO Yuji

Registration info

オンライン

Free

Attendees
7

Attendees
YAMAMOTO Yuji
Satoshi Takimoto
えび
shnarazk
pomera
khibino
yukiyama1335
View Attendee List
Start Date
2024/02/26(Mon) 20:00 ~ 22:00
Registration Period

2024/02/12(Mon) 22:03 〜
2024/02/26(Mon) 22:00まで

Location

Discord

オンライン

参加者への情報
(参加者と発表者のみに公開されます)
出席登録
(イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます)

Description

「LEAN勉強会」というDiscordのサーバーが既にあったので、区別するために名前を変更しました。ご容赦ください。

内容・動機

Software Foundations vol. 1 Logical Foundationsという著名な本のサンプルコードを、主催である私YAMAMOTO Yujiと喋りながらCoqからLean 4に翻訳して、Lean 4を勉強します。 私はSoftware Foundations vol. 1の大半を読み終え、大雑把に内容を把握しましたが、まだ手を動かせていないので、みなさんからアドバイスを得ながらCoqをLean 4に翻訳することで、定理証明支援系の使い方などを学びたいと考えています。

今回は演習問題: ★, standard (factorial)の節から始めます。

参加方法

このイベントに参加登録すると見える「参加者への情報」に、専用のDiscordサーバーへの招待リンクを作成しましたので、そちらからご登録ください。こちらのDiscordサーバーのボイスチャンネルで行う予定です。

Lean開発環境の準備

「いっしょに進めたい!」という方は https://github.com/leanprover/lean4/blob/master/doc/quickstart.md に書かれている手順に従って、Lean 4のVS Code向け拡張をインストールすると、私と同じ方法でセットアップできるのでお勧めです。

Media View all Media

If you add event media, up to 3 items will be shown here.

Feed

YAMAMOTO Yuji

YAMAMOTO Yuji published SF.lean勉強会.

02/12/2024 22:03

SF.lean勉強会 を公開しました!

Ended

2024/02/26(Mon)

20:00
22:00

Registration Period
2024/02/12(Mon) 22:03 〜
2024/02/26(Mon) 22:00

Location

Discord

オンライン

Discord

Organizer

Attendees(7)

YAMAMOTO Yuji

YAMAMOTO Yuji

SF.lean勉強会 に参加を申し込みました!

Satoshi Takimoto

Satoshi Takimoto

SF.lean勉強会 に参加を申し込みました!

えび

えび

SF.lean勉強会 に参加を申し込みました!

shnarazk

shnarazk

SF.lean勉強会 に参加を申し込みました!

pomera

pomera

SF.lean勉強会 に参加を申し込みました!

khibino

khibino

SF.lean勉強会 に参加を申し込みました!

yukiyama1335

yukiyama1335

SF.lean勉強会 に参加を申し込みました!

Attendees (7)