-
yoshihiro503
- 1950
- 6
- 1
- 0
-
- いいね！0
Masaki Hara
@qnighy
A -> B -> Prop を A -> m B とみてるわけだから、やっぱりpowerset(か、濃度を高々1に制限したpowerset=古典的にはMaybeと同型)と見るとしっくりくるような…… #ProofSummit2016
2016-09-25 14:13:48
Yoshihiro Imai
@yoshihiro503
「Fiatにはrefineという型コンストラクタがある」 #ProofSummit2016 #Fiat #coq
2016-09-25 14:15:57
Keigo Imai
@keigoi
plv.csail.mit.edu/fiat/ の examples みてたら refine なんとかって出てきますね #ProofSummit2016 たぶん微分はない
2016-09-25 14:19:00
Keigo Imai
@keigoi
FiatのCompは存在するかどうかわからんものを入れておいて別個でrefine使って証明を与えるとExtractできるアルゴリズムを取り出せるコンテナ #ProofSummit2016 でいいのかな。
2016-09-25 14:27:05
Sosuke MORIGUCHI
@chiguri
量化子除去、有理数や実数は比較的簡単にいくが、整数だと係数を揃えるのと、述語（divisibleみたいなものか）が必要なのが問題。 #ProofSummit2016
2016-09-25 14:54:01
でこれき
@dico_leque
coq-contribs/high-school-geometry: Geometry for French high-school github.com/coq-contribs/h… みたいなのはあった #ProofSummit2016
2016-09-25 15:24:15
Yoshihiro Imai
@yoshihiro503
「posix regular expression parsingの話をします」 #proofsummit2016
2016-09-25 15:27:04
Sosuke MORIGUCHI
@chiguri
POSIX regular expression parsing with derivativesを検証したい、ということらしい。 #ProofSummit2016
2016-09-25 15:27:50
Akira Sugiura
@urasandesu
あー、京都だったのか。知ってても予定合わなかったっぽい。次こそは…！ (｀・ω・´) Proof Summit 2016 - connpass proof-summit.connpass.com/event/34848/
2016-09-25 15:42:46
Keigo Imai
@keigoi
正規表現マッチ同士が incomparable なのはどういうケースだったんだろうか（そんなのある？） #ProofSummit2016
2016-09-25 15:54:30
でこれき
@dico_leque
>ᵣ の定義は p.4。 Left vs. Right は A1, A2 で、 len の比較に等号が入るかどうか。 Right vs. Right, Left vs. Left は単に >ᵣ で比べる #ProofSummit2016
2016-09-25 15:55:45
Yoshihiro Imai
@yoshihiro503
CoqでもRegExpを検証した話があったような... #proofsummit2016 lix.polytechnique.fr/coq/pylons/con…
2016-09-25 15:56:52
Yoshihiro Imai
@yoshihiro503
「VeriFastはCとかJavaとかの検証器。separation logicというホーア論理の拡張を使って検証する。自動化はあんまりないから人間ががんばれ」 #proofsummit2016 #VeriFast
2016-09-25 16:04:38