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

Agda

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

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

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

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

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

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

ネットで話題

もっと見る
69ブックマーク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」の研修コースを産総研が開催 | スラド デベロッパー産業技術総合研究所により、関数型プログラミング言語「Agda」の研修コースが開催されるそうです（産総研：システム検証研究センター：CVS研修コース「Agdaによる仕様記述」）。 Agdaは強力な依存型を備えた関数型プログラミング言語であり、証明支援システムとして利用できることでも知られています。また、その形式手...developers.srad.jp
13ブックマークAgda ハンズオン活動報告www.klab.com
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ブックマーク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

関連ブログ

opfer_10155’s diary•2 年前

依存型を使った、型安全な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•2 年前

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

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

#Agda#ラムダ計算#インタプリタ#依存型#型システム
朝日ネット　技術者ブログ•3 か月前

Haskellと余代数(Coalgebra)

ここではHaskellの中級者向けのトピックを簡単に取り上げたいと思います。 今回は余代数(Coalgebra)についてです。Haskellを書いていると『余（なんとか）』という言葉をみかけることがあります。これは英語の接頭辞 Co- の訳で、ここでは代数(Algebra)の双対(Dual)という意味で余代数と呼ばれています。 さてHaskellやOCamlのデータ型は一般に代数的データ型(Algebraic data type)と呼ばれます。このデータ型にパターンマッチングを加えて、（オブジェクト指向言語などと比較したときの）関数型言語の特徴と紹介されることも多いと思います。実はこのデータ型…

niming538の日記•4 か月前

プログラミング言語Elixir事始め

メモ elixir のインストール。windows , mac 共に基本的には elixir 本家の通り。 mac の場合、appleシリコン用 homebrew をインストールしてから brew を使った。 windows の場合は chocolatey をインストールしてから使った。 chocolatey をインストールする際、PowerShell を 7 に upgrade した。 えっと暫く前までお金がなくて安い中古マシンにUbuntuをインストールして生活していました。10年程。 それで不便があったわけではないのですが、70歳で年金が出るようになって若干生活に余裕が出てきたのでWin…

Svelandski氏の秘められた日記•5 か月前

腰痛の原因を探る

2022-02-05 (土)（令和4年壬寅）<旧暦 1 月 5 日>（大安 己丑 八白土星） Agata Agda 第 5 週 第 26666 日 この頃やうやく腰痛が収まってきた感じがある。それでもなんとか痛さを我慢できる程度なのであって、すっかり良いわけではない。僕の場合、この腰痛の原因はどこにあるのかを色々と考へてみたのだが、ひとつの結論に至った。それは机に向かって座る時の姿勢が悪いのである。ゲームをするわけではないが、僕は起きてゐる時間のほとんどはコンピュータに向かってゐる。その間に腰に無理な力がかかってゐるのだと思ふ。実は自転車のサドルのようなものを椅子の上に置いて座ってゐる。これは…

Acme::AnaTofuZ->new;•昨年

TypeScriptで関数合成をする関数を書いてみた

関数型プログラミングといえば関数合成みたいなところありますよね。Haskellだと.でagdaだとoだった気がする。 最近やっているTypeScriptで関数合成をやってみました。 以下はググって出てきたこのサイトを参考にしています。 minaluke.medium.com まず例題のために簡単なInterfaceを定義してみます。 nameというフィールドがあってstringが入っています。 interface IPerson { name: string; } const person: IPerson = { name: "Mina", }; ここから次の関数を順に実行することを考えます…