[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 (応援スレ) 63 (1002ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
80(4): 2021/12/29(水)17:51 ID:00LaB1j1(1) AAS
>>81-90
一応置きあグロ
167: 2021/12/29(水)22:29 ID:F3ixTfm/(1) AAS
a_watcherが>>75,78,80に感銘を受けた事を確認
174(1): 2021/12/30(木)08:01 AAS
>>166
>80年代から定理証明系に興味を持ち、
>一度はそちら方面の専攻を考えた(一応誘われた)者
なるほど しかしそれは論理学もしくは情報科学であって
数論ではありませんね
>M氏の仕事を一般報道で初めて知った時、
>数学の形をとったモジュラー・プログラミング的な物
>(あるいは数学系のセンスではオブジェクト指向プログラミング的な物)
>なのだろうという我流の理解をした
一つ質問ですが、圏論ではそういう
省6
186(1): 2021/12/30(木)09:25 AAS
>>181
20世紀の情報科学か、なにもかもみな懐かしい…
>その当時の学生にとっては、
>80年代は定理証明系と型を命題と捉えた
>カリー=ハワード同型対応プログラミング
>がせいぜいの所
90年代だったと思いますが、当時龍谷大にいた小林聡氏が
「実は古典論理でもカリー・ハワード対応で
プログラム抽出できる」
という話をして
省9
188(1): 2021/12/30(木)09:30 AAS
昔話、つづけますか
>>181
>80年代国内ではcoq以前にMisarという処理系を先行導入している研究室があって、
信州大学の中村八束さんでしたっけ？
>ハギャ先生一行がその研究室を訪問した記録には心を躍らせていた
萩谷昌己氏ならよく存じあげていますよ
7bitsのThemskyのm氏でしょ
「止まれ！」は実にいい解説文でしたね
巨大数愛好家の人はぜひ読んでほしいな
動画ﾘﾝｸ[YouTube]
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.296s*