17/06/09 16:51:44.77 VCuqCK40.net
おおおわかった気がする
ありがとう！
なんでも再起とやらも読んで見ることにする
982:デフォルトの名無しさん
17/06/09 17:05:35.04 3Dqy8l+L.net
>>968
return f_inner(n, 1)
じゃない？
983:デフォルトの名無しさん
17/06/25 18:30:26.47 v1ZjLLZV.net
OcamlとかCoqって名古屋以外でも大学での授業とか研究に使われているの？
一時期のブームは去ったみたいだけど。
大学の情報学部とかの現状にはちょっとだけ興味がある。
そして流行に後れて今頃勉強している40代のオレ。
984:デフォルトの名無しさん
17/07/03 09:21:46.88 ipQv+IYB.net
東大東北大お茶の水では使ってた
985:デフォルトの名無しさん
17/07/03 17:44:24.93 /M1wO8+Z.net
授業で使ったのに広まらなかったということか。
つまり啓蒙に失敗したと。
986:デフォルトの名無しさん
17/07/04 13:46:26.44 VgVQ93XC.net
Occamなら知っとるぞよ？
987:デフォルトの名無しさん
17/07/12 14:21:04.56 06OhWRFP.net
>973
広まらなかったというかキラーアプリがなかったというか…
結局Ocamlで作られたアプリで唯一プログラマ間で流行ったのがCoqなんじゃね？
988:デフォルトの名無しさん
17/07/12 14:33:02.68 bLDjTsNM.net
OCaml は金融とかで使われてるんじゃ無かったか。
そういや Rust も最初は OCaml でコンパイラー書かれてたんだよな。
989:デフォルトの名無しさん
17/07/14 23:08:50.92 UJz0OWoz.net
俺がocaml覚えたきっかけはとあるエロゲーのチートツールなんだが
あれの作者がなぜそれを採用したかにはずごい興味ある
990:デフォルトの名無しさん
17/07/15 12:06:36.80 03i9G/wL.net
>>977
どっかの学生だったんじゃないの？兄妹ものエロゲだけに京大とか。
991:デフォルトの名無しさん
17/08/16 21:00:55.34 H/HIEf+2.net
(*´・ω・`*)
992:デフォルトの名無しさん
17/08/17 13:02:39.82 5mQoD0+b.net
(´・ω・｀)
993:デフォルトの名無しさん
17/09/01 18:43:59.45 RxXe6GrD.net
8月はちょっと纏まった時間がとれたので、
「ソフトウェアの基礎」日本語訳の練習問題を解きすすめてみた。
まだPoly.vが終わった序盤だけどだいぶCoqに慣れてきた。
星三つrecommendedでもたまに難しい問題があるなー、というのが感想。
論理学の命題というのは高校・大学教育で慣れているだけで
見直してみると思ったよりも複雑な構造をしていたのだと今更ながらに感じた。
実務でCoqが要求されることは当分ないと思うけど、
逆変換の関数は少なからず実装することがあるので
ときどき「Coｑ使って証明したい」という気分にはなるんだよなー。
994:デフォルトの名無しさん
17/09/05 11:03:28.55 a/Cb1ZW9.net
URLﾘﾝｸ(ocaml.jp)
死んでるな……
> ( ! ) Parse error: syntax error, unexpected 'new' (T_NEW) in /virtual/osiire/public_html/lib/func.php on line 531
995:デフォルトの名無しさん
17/09/08 14:02:07.35 swD2wqBn.net
ocaml.jpは息してる？
996:デフォルトの名無しさん
17/09/24 12:35:45.27 VL5Szw+L.net
いつまで死んでるんだよ
997:デフォルトの名無しさん
17/10/03 00:31:09.35 JZnIdnEQ.net
復活した
998:デフォルトの名無しさん
17/10/03 02:20:47.65 upqeSfz9.net
復活したのは良いけど、一言何か無いのかよ。誰が管理してるんだ。
999:979
17/10/05 12:08:08.18 SZzrAZT5.net
日本語訳の古さに苦戦しつつLogic.vまで進めていたところ……
久しぶりに英語の本家を見たら、
なんかVol.1 ～ Vol.3に増えてるー！？
あまりの道のりの遠さに絶望しつつ内容を見ると、
旧版からホーア理論まわりをVol..2に分離し、
Vol.3は赤黒木等の少し高度なデータ構造について色々とCoqで証明して感じらしい（新規）。
……く、面白そうじゃないか。
1000:デフォルトの名無しさん
17/10/05 19:45:51.56 72rIdNeW.net
>>981
リンクpls
1001:デフォルトの名無しさん
17/10/07 12:06:25.63 689sKi0/.net
>>988
URLﾘﾝｸ(softwarefoundations.cis.upenn.edu)
1002:979
17/10/30 19:39:25.32 asGH9s/c.net
ここ一ヶ月、旧くなった日本語版を捨て英語版に再挑戦してみた。
以前は出来るだけ写経していたが時間がかかり過ぎるので、
付属の.vファイルを直接書き換える方針に変更。
結構章立てと共に内容変わってるなぁ……追加された良問も多いし。
英語の非形式的証明は書く機会もなさそうだし、パスするか。
しかし、答えがWeb上に転がってないのは自習者には正直辛い。
どうもSICPみたいな標準教科書を目指してるっぽい？
こーゆうの(coq)を国立研究所で作れる国はやっぱり凄いと思う今日この頃。
1003:デフォルトの名無しさん
17/11/01 07:27:01.78 wuKEf1Sh.net
a
1004:デフォルトの名無しさん
17/11/01 07:27:36.60 wuKEf1Sh.net
sit
1005:デフォルトの名無しさん
17/11/01 07:27:56.41 wuKEf1Sh.net
dot
1006:デフォルトの名無しさん
17/11/01 07:28:13.79 wuKEf1Sh.net
egg
1007:デフォルトの名無しさん
17/11/01 07:28:31.25 wuKEf1Sh.net
nø
1008:デフォルトの名無しさん
17/11/01 07:28:48.81 wuKEf1Sh.net
this
1009:デフォルトの名無しさん
17/11/01 07:29:26.33 wuKEf1Sh.net
combi
1010:デフォルトの名無しさん
17/11/01 07:30:08.09 wuKEf1Sh.net
it
1011:デフォルトの名無しさん
17/11/01 07:30:42.85 wuKEf1Sh.net
2
1012:デフォルトの名無しさん
17/11/01 07:31:16.98 wuKEf1Sh.net
ping
1013:デフォルトの名無しさん
17/11/01 07:32:05.81 wuKEf1Sh.net
pong
1014:デフォルトの名無しさん
17/11/01 07:32:32.73 wuKEf1Sh.net
wild
1015:1001
Over 1000 Thread.net
このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 3061日 0時間 17分 11秒
1016:過去ログ ★
[過去ログ]
■ このスレッドは過去ログ倉庫に格納されています