九州大学論理と計算研究室関係計算の形式化を用いた数学とソフトウェア検証のための理論構築

講演スライド等

関係計算理論
記号計算・グラフ理論・セルオートマトン
圏論とその応用
定理証明支援系

1. 関係計算理論

Theory of Relational Calculus and its Formalization (USMac2016)

A Coq Library for the Theory of Relational Calculus (Univ. Hawaii 2015)

Theories of Relations (Pusan National University 2011)

read more
（前半）read more
（後半）

2. 記号計算・グラフ理論・セルオートマトン

Symbolic Computations in Conformal Geometric Algebra for Three Dimensional Origami Folds (2016)

Verification of a brick wang tiling algorithm (2016)

Graph partitioning and characteristic polynomials of Laplacian matrics of Roach-type graphs (2013)

Generalization of Compositons of Cellular Automata on Groups (2011)

3. 圏論とその応用

Algebras for programming languages (2015)

圏論のモナドとHaskellのモナド (2005)

4. 定理証明支援系

定理証明支援系Coqについて (2015)

Coq関係計算ライブラリの開発と写像の性質の証明 (2015)

Coqチュートリアル (2015)

有限オートマトンとスティッカー系に関するCoqによる形式証明について (2014)

Verification of a brick wang tiling algorithm (2016)

5. 高校生向け解説

数式処理ソフトMathematicaで数学の問題を解く(2016)

計算機を用いて数学の問題を解くということ (2015)

計算可能実数とは (2006)

グラフデータ構造と５色定理 (2013)

行列計算を利用したデータ解析技術 (2012)

複素数・四元数と図形の回転 (2013)

6. 計算機関係の技術情報

Overleafを使った日本語LaTeX文書作成 (2020)

Homebrewによるソフトウェアの実装(1) (2020)

① Homebrew (MacOS用パッケージマネジャー
② Emac ( テキストエディタ)
③ Haskell (関数型言語)
④ MacTeX 文書処理システム)
⑤ YaTeX (野鳥: Emacs TeXモード)

Homebrewによるソフトウェアの実装(2) (2020)

①CoqIDE (Coq定理証明支援システム)
②MathCom (形式証明ライブラリ

Homebrewによるソフトウェアの実装(3) (2020)

① Anaconda (Spyder) (Python開発環境プラットフォーム)
② pandas (Python用データ処理関数ライブラリ)
③ Matplotlib (Python用データ描画関数ライブラリ)
④ IPAexフォント (オープンソース日本語語フォント)

Mac bookでwebサーバーを起動する方法 (2014)

Amazon AWSの使い方 (2018)