- 1 名前：デフォルトの名無しさん mailto:sage [2009/06/15(月) 07:15:21 .net]
- 関数型言語MLについて語るスレッドです。
MLは、確固とした理論的背景を持つ言語でありながら、
現実的なソフトの開発にも使用できる実用性を備えた言語です。
また、プログラミングの初心者が最初に学習する言語としても優れています。
総本山
Standard ML www.smlnj.org/
Objective Caml caml.inria.fr/ocaml/
前スレ
関数型言語ML(SML, OCaml, etc.), Part 5
pc12.2ch.net/test/read.cgi/tech/1186292994/
- 992 名前：デフォルトの名無しさん mailto:sage [2017/08/17(木) 13:02:39.82 ID:5mQoD0+b.net]
- (´・ω・｀)
- 993 名前：デフォルトの名無しさん mailto:sage [2017/09/01(金) 18:43:59.45 ID:RxXe6GrD.net]
- 8月はちょっと纏まった時間がとれたので、
「ソフトウェアの基礎」日本語訳の練習問題を解きすすめてみた。
まだPoly.vが終わった序盤だけどだいぶCoqに慣れてきた。
星三つrecommendedでもたまに難しい問題があるなー、というのが感想。
論理学の命題というのは高校・大学教育で慣れているだけで
見直してみると思ったよりも複雑な構造をしていたのだと今更ながらに感じた。
実務でCoqが要求されることは当分ないと思うけど、
逆変換の関数は少なからず実装することがあるので
ときどき「Coｑ使って証明したい」という気分にはなるんだよなー。
- 994 名前：デフォルトの名無しさん mailto:sage [2017/09/05(火) 11:03:28.55 ID:a/Cb1ZW9.net]
- ocaml.jp/
死んでるな……
> ( ! ) Parse error: syntax error, unexpected 'new' (T_NEW) in /virtual/osiire/public_html/lib/func.php on line 531
- 995 名前：デフォルトの名無しさん mailto:sage [2017/09/08(金) 14:02:07.35 ID:swD2wqBn.net]
- ocaml.jpは息してる？
- 996 名前：デフォルトの名無しさん mailto:sage [2017/09/24(日) 12:35:45.27 ID:VL5Szw+L.net]
- いつまで死んでるんだよ
- 997 名前：デフォルトの名無しさん mailto:sage [2017/10/03(火) 00:31:09.35 ID:JZnIdnEQ.net]
- 復活した
- 998 名前：デフォルトの名無しさん mailto:sage [2017/10/03(火) 02:20:47.65 ID:upqeSfz9.net]
- 復活したのは良いけど、一言何か無いのかよ。誰が管理してるんだ。
- 999 名前：979 mailto:sage [2017/10/05(木) 12:08:08.18 ID:SZzrAZT5.net]
- 日本語訳の古さに苦戦しつつLogic.vまで進めていたところ……
久しぶりに英語の本家を見たら、
なんかVol.1 〜 Vol.3に増えてるー！？
あまりの道のりの遠さに絶望しつつ内容を見ると、
旧版からホーア理論まわりをVol..2に分離し、
Vol.3は赤黒木等の少し高度なデータ構造について色々とCoqで証明して感じらしい（新規）。
……く、面白そうじゃないか。
- 1000 名前：デフォルトの名無しさん mailto:sage [2017/10/05(木) 19:45:51.56 ID:72rIdNeW.net]
- >>981
リンクpls
- 1001 名前：デフォルトの名無しさん mailto:sage [2017/10/07(土) 12:06:25.63 ID:689sKi0/.net]
- >>988
https://softwarefoundations.cis.upenn.edu/
- 1002 名前：979 mailto:sage [2017/10/30(月) 19:39:25.32 ID:asGH9s/c.net]
- ここ一ヶ月、旧くなった日本語版を捨て英語版に再挑戦してみた。
以前は出来るだけ写経していたが時間がかかり過ぎるので、
付属の.vファイルを直接書き換える方針に変更。
結構章立てと共に内容変わってるなぁ……追加された良問も多いし。
英語の非形式的証明は書く機会もなさそうだし、パスするか。
しかし、答えがWeb上に転がってないのは自習者には正直辛い。
どうもSICPみたいな標準教科書を目指してるっぽい？
こーゆうの(coq)を国立研究所で作れる国はやっぱり凄いと思う今日この頃。
- 1003 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:01.78 ID:wuKEf1Sh.net]
- a
- 1004 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:36.60 ID:wuKEf1Sh.net]
- sit
- 1005 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:27:56.41 ID:wuKEf1Sh.net]
- dot
- 1006 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:13.79 ID:wuKEf1Sh.net]
- egg
- 1007 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:31.25 ID:wuKEf1Sh.net]
- nø
- 1008 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:28:48.81 ID:wuKEf1Sh.net]
- this
- 1009 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:29:26.33 ID:wuKEf1Sh.net]
- combi
- 1010 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:30:08.09 ID:wuKEf1Sh.net]
- it
- 1011 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:30:42.85 ID:wuKEf1Sh.net]
- 2
- 1012 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:31:16.98 ID:wuKEf1Sh.net]
- ping
- 1013 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:32:05.81 ID:wuKEf1Sh.net]
- pong
- 1014 名前：デフォルトの名無しさん mailto:sage [2017/11/01(水) 07:32:32.73 ID:wuKEf1Sh.net]
- wild
- 1015 名前：1001 [Over 1000 Thread.net]
- このスレッドは１０００を超えました。
新しいスレッドを立ててください。
life time: 3061日 0時間 17分 11秒
- 1016 名前：過去ログ ★ [[過去ログ]]
- ■ このスレッドは過去ログ倉庫に格納されています
|
 |
