Agda ハンズオン活動報告
こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。 はじめに Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2 と n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。 KLab では月に１回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agd
Learn You an Agda - William DeMeo
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
安全かつ柔軟な依存型 -
この記事はTheorem Proving Advent Calendar 2011の1日目の記事です。 今日は Agda2 というプログラミング言語を用いて、依存型を用いることで絶対的な安全性と Haskell や OCaml などでは(通常の方法では)実現できない柔軟さのどちらも持つプログラムを記述できるということについて書きます。 この記事は主に、普段動的型付けのプログラミング言語を使っていて、静的型付きの言語では自分の意図したものを十分に表現できないと考えている人を対象読者としています。 依存型とは 型に依存する型や、値に依存する型を作れる型のことです。 例えば、値に依存する型を用いることで型レベルでサイズが与えられているリストを作ることが可能です。 また、リストの結合関数は長さ a のリストと長さ b のリストを取り、リスト a+b のリストを返すというような型を持つことになります
はてなブログ | 無料ブログを作成しよう
聖蹟桜ヶ丘へ 今年度の授業が全て終了した。最後の授業はテスト返却とその確認作業の後は特に何をしろとも言われていなかったので、『耳をすませば』の後半、お姉さんと雫が言い争いをする場面を生徒と皆で見た。 この場面。あの場面、お姉さんは雫に「今しなきゃいけないことから逃…
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
