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

Agda

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

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

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

AGDA新人賞展2022＠クリエイションギャラリーG8　2022年6月4日（土）

受賞者は『佐々木拓・竹田美織・前原翔一』の三名。 中でも『佐々木拓』による文房具関連展示がツボ。 最近はリモートワークにより出社の機会が激減とは言え、数十年に渡り身近に在ったモノを新たな意匠で魅せられると普段とは違う印象を持つから何とも不思議。 会期は～7月2日（土）まで。

#クリエイションギャラリーG8#新人賞#無料の展覧会

ネットで話題

もっと見る
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年前

依存型を使った、型安全な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#ラムダ計算#インタプリタ#依存型#型システム