labg:emoto-lab:jssst2019
差分
このページの2つのバージョン間の差分を表示します。
| 次のリビジョン | 前のリビジョン | ||
| labg:emoto-lab:jssst2019 [2019/09/04 14:13] – 作成 emoto | labg:emoto-lab:jssst2019 [2019/09/06 14:50] (現在) – murata | ||
|---|---|---|---|
| 行 1: | 行 1: | ||
| - | ====== 神野君の発表 | + | |
| + | 以下、発表の質疑周りのメモ | ||
| + | |||
| + | ==== 村田君の発表 ==== | ||
| + | |||
| + | * 東大の森畑先生 | ||
| + | * Regular Functor も行く？ cata_charn の証明を与えるなら、他の functor でもいいんじゃない？ polynomial functor に限らなくてもいいよね。 | ||
| + | * initial_algebra が一般的な functor を型クラスのインスタンスで受け取るようにしておいて、polynomial functor については cata_charn を自動証明して initial_algebra のインスタンスを生成するようなものを用意しておくとか。 | ||
| + | * Adjoint fold/ | ||
| + | * Hylo が…… | ||
| + | * hylo できないのは残念ですね。 | ||
| + | * Rel でやらなかったん？ Coq の関数を rel に見て、ゴニョゴニョして戻ってこれればいいんじゃない？ | ||
| + | * まあ、うまく戻ってくるのが簡単ではなさそうなので、とりあえず別にしてます。 | ||
| + | * Haskell の deriving みたいな？ ADT定義から色々出せるといいけどね。 | ||
| + | * Coq 自体に手を入れればできるだろうけど…… テンプレート Coq があればいいのだろうか。 | ||
| + | * 実はそれらしきものは発見しているのだが、まだ全然追えていないです by muratak | ||
| + | * https:// | ||
| + | * そして、プログラム変換は何ができたらいいんだろうね、と。 | ||
| + | * 少し先のものなら、polynomial を regular とかにしようか？ join list とか rose tree とか。すぐに polynomial じゃ無くなっちゃうから。 | ||
| + | |||
| + | * 東大の佐藤先生（黒い佐藤さん） | ||
| + | * Coq で generic programming はよくあること？ Coq 本に何かあったような？ | ||
| + | * Certified Programming with Dependent Types に何かあったような。 | ||
| + | |||
| + | ==== 神野君の発表 ==== | ||
| * 筑波大学の長谷部先生 | * 筑波大学の長谷部先生 | ||
labg/emoto-lab/jssst2019.1567573987.txt.gz · 最終更新: 2019/09/04 14:13 by emoto