Hatena Blog Tags
はてなブログ トップ
Agda
このタグでブログを書く
言葉の解説
ネットで話題
関連ブログ

Agda

(コンピュータ)
【あぐだ】

定理証明機。依存型がすごいらしい。

このタグの解説についてこの解説文は、すでに終了したサービス「はてなキーワード」内で有志のユーザーが作成・編集した内容に基づいています。その正確性や網羅性をはてなが保証するものではありません。問題のある記述を発見した場合には、お問い合わせフォームよりご連絡ください。
kohagura's blog•1年前

Agdaを使った命題 A -> A の証明

Agdaを使った命題 ( A -> A ) の証明 はじめに Agdaは型理論に基づく関数型プログラミング言語であり、定理証明支援ツールとしても利用されています。この記事では、基本的な命題 ( A -> A ) をAgdaを使って証明する方法を説明します。この命題は、「Aが成り立つならばAが成り立つ」という自己明白な命題です。 1. Agdaの基本的な概念 まず、Agdaの型システムの基本的な概念を理解することから始めましょう。Agdaでは、型（Type）と値（Value）が重要な役割を果たします。 型（Type）: 値の集合を表します。例えば、Bool はブール値（true または fals…

#Agda

ネットで話題

もっと見る
70ブックマークAgda による圏論入門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 と圏の入門 ...ie.u-ryukyu.ac.jp
43ブックマーク未来言語Agda - 数学猫の生活と意見最近Agdaを触る機会があったのだが、Agdaこそ未来のプログラミング言語ではないかという気がしてきた。ここでは行列の転置をする関数を定義することで、Agdaでのプログラミングがどんなものか紹介したい。その前に一言:Agdaは定理証明系として紹介されることが多い。これはAgdaにとって不幸なことだ。確かにAgdaの型シス...d.hatena.ne.jp
17ブックマークThe Agda WikiAgda 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 assi...wiki.portal.chalmers.se
13ブックマークAgda ハンズオン活動報告www.klab.com
13ブックマーク関数型プログラミング言語「Agda」の研修コースを産総研が開催 | スラド デベロッパー産業技術総合研究所により、関数型プログラミング言語「Agda」の研修コースが開催されるそうです（産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」）。 Agdaは強力な依存型を備えた関数型プログラミング言語であり、証明支援システムとして利用できることでも知られています。また、その形式手...developers.srad.jp
12ブックマークLearn You an Agda - William DeMeoThis 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}...williamdemeo.github.io
12ブックマークLearn you An Agda And Achieve EnlightenmentRead It!learnyouanagda.liamoc.net
9ブックマークAgda 入門＠ProofSummit 2011www.slideshare.net
8ブックマークProgramming Language Foundations in Agda – Table of ContentsThis book is an introduction to programming language theory using the proof assistant Agda. Comments on all matters—organisation, material to add, material to remove, parts that require better explanation, good exercises, errors, and typos—are welcome. The book repository is on GitHub. Pull reque...plfa.github.io

関連ブログ

opfer_10155’s diary•5年前

スコープとフレームを使った変数束縛

PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についてのまとめ 初めての人は最初の記事をまず読んで欲しい 前回のおはなし ソースコードはこれ github.com 参考: - 束縛変数 --筑波大学 スコープグラフ(scope graph)は静的束縛(lexical binding)と 動的束縛(non-lexical binding)の両方をサポートする静的名前解決の統一的アプローチ(uniform approach)です。 今回は、スコープグラフとヒープフレームをIntrinsi…

#Agda#インタプリタ
opfer_10155’s diary•5年前

依存型を使った、型安全なMutable Stateを扱うインタプリタ(STLC+Ref)

PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についての輪講で、発表の際に使用したスライドの供養(ブログ用に多少修正は加えている) 初めての人は前回のおはなしをまず読んで欲しい ソースコードはこれ github.com 正直この章はめちゃくちゃしんどかったが、がんばって噛み砕いで説明した。 実際この論文は本当によく書かれていて、多少前提知識がなくても気合いがあれば調べながら大筋は理解できるようになっている。 参考: - What is Agda? -- Agda docs 依存型につ…

#Agda#Interpreter#インタプリタ#型システム#モナド
opfer_10155’s diary•5年前

依存型による単純型付きλ計算(STLC)のインタプリタ

PoPLの論文(Intrinsically-Typed Definitional Interpreters for Imperative Languages)についての輪講で、発表の際に使用したスライドの供養(ブログ用に多少修正は加えている) ソースコードはこれ github.com Agdaを知らなくても、Haskellの入門程度の知識と、コードを読む力と気合いがあればわかります。 この手の話に興味がある人は面白く感じることでしょう。 つぎのおはなし 参考: - What is Agda? -- Agda docs 型付きラムダ計算 -- 筑波大学 依存型について -- hatenablog…

#Agda#ラムダ計算#インタプリタ#依存型#型システム