形式手法

MaruLabo Micro Media -- MMM
Coq スタートアップセミナー (1)

2021/06/27 第一回「Coq環境の紹介」 講演資料 ダウンロード 講演動画

続きを読む
マルゼミ
MIP*=RE 入門-- Interactive Proofとnonlocal ゲーム --

2020/12/25 マルゼミ 「MIP*=RE 入門」概要 このセミナーですが、次のような構成を考えています。 第一部「Nonlocal Game-- エンタングルメントとゲーム」では、アインシュタインらの「 隠れた […]

続きを読む
マルレク
人工知能と計算科学 -- 計算複雑性入門

2020/09/18 マルレク「人工知能と計算科学」概要 今年、「計算複雑性」という数学の一分野で大きな発見がありました。「それって、ITの世界と何か関係があるの?」と感じる人も多いと思います。確かに直接的にはたいした関 […]

続きを読む
マルレク
AWSでの形式手法の利用

2020/05/05 マルレク「AWSでの形式手法の利用」概要 今回のマルレクのテーマは、「AWSでの形式手法の利用」です。 この間、 形式手法を開発者に広めたいと思って、いろいろ試行錯誤をしてきたのですが、開発者にとっ […]

続きを読む
マルゼミ
論理学入門 II -- ラムダ計算と関数型言語

2020/03/27 マルゼミ「論理学 II」概要 「論理学 I」との関係について 前回の「論理学 I — 命題論理の演繹ルール」では、「推論する能力」の最も基本的な基礎である、論理的推論ルールにフォーカスしました。今回 […]

続きを読む
マルゼミ
論理学入門 I -- 命題論理の演繹ルール

2020/01/28 マルゼミ「論理学入門 I」概要 なぜ今「論理学」を学ぶのか? その理由は、人工知能技術の未来に関係しています。丸山は、人工知能技術の次の飛躍は、コンピュータの論理的に推論する能力が、現実の課題に広く […]

続きを読む
マルレク
IT技術とCoqの世界 --証明 = プログラム = 計算の意味を考える

セミナーの呼びかけ プログラマーは考える。プログラミングは論理的である Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野(数学の問題の証明等)での特殊なコンピュータの […]

続きを読む
その他講演
はじめてのCoq

Coq Tutorial https://github.com/maruyama097/coq-tutorial 概要 https://coq-handson.peatix.com/ 目次 I. Hello Coq! C […]

続きを読む
人工知能
プログラムと論理

2019/10/10 マルレク・サブゼミ 概要:https://programlogic.peatix.com/ 資料ダウンロード:http://bit.ly/35iljUn 資料viewer 「はじめに」から 小論は、 […]

続きを読む
マルレク
ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界

2019/9/24 マルレク 概要:https://deep-spec.peatix.com/ 資料ダウンロード:http://bit.ly/2muEmcl 資料viewer 「はじめに」から 小論の目的は、ソフトウェア […]

続きを読む