こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。 はじめに Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2 と n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。 KLab では月に１回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agd
This is a markdown version of the tutorial Learn You an Agda and Achieve Enlightenment! by Liam O’Connor-Davis. I made this version for my own reference, while working through the tutorial, making some revisions and additions, and a few corrections. You may prefer the original. $\def\N{\mathbb N} \def\true{\mathsf{true}} \def\conj{\wedge} \def\disj{\vee}$ Table of Contents 1. Introduction About th
カリー＝ハワード同型対応とか難しい事は分からんが、型と証明が一対一で対応するらしい。 型理論の枠組みの中でプログラミングを行おうとする言語には、証明が出来るものがある。 という事で、Agdaというプログラミング言語を習得しようとインストールしてみた。 ここに書いてあることの大体は[Agda Wiki][agda-wiki]という所に書いてある。 というかAgdaに必要な知識の大体はここに書いてある。(英語の読めない自分には辛いけど。) 自分の環境はMac(Homebrew導入済み)なので、これを前提に進めていく。（というか、Debian系ディストリビューションにはパッケージがあるらしい…） Haskell-Platformのインストール Homebrewを使ってhaskell-platformをインストールする。 brew install haskell-platform これだけ。ghc
2014/07/17 講義記録 2014/07/10 第12回講義 2014/07/03 第11回講義 2014/06/26 第10回講義 2014/06/19 第9回講義 2014/06/12 第8回講義 トップページ test 第７回講義 2014/05/29 第6回講義 2014/05/28 第３回講義 第２回講義 2014/05/27 第５回講義 2014/05/15 インストール 第４回講義 2014/05/02 コマンド一覧 2014/04/24 記号 第１回講義 2014/04/20 メニュー 2014/04/17 編集用テンプレート
Menu Menu Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。 Higher-Order Categorical Logic の 0章に相等する内容です。 BitBucket category-exercise-in-agda source code Agda の入門の要約 Agda の入門 Agda の集合の Level Agda の record Agda のReasoning Caategory module と圏の入門 自然変換 IdentityFunctor と Hom Reasoning Monad の結合則 Sets と Monoid を使った Monad の例 Kleisli 圏の構成 ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。 Adjoint から Monad を導く Kleisli 圏による Mona
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for wr
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
