Xavier Leroy - Home page
Hello and welcome to my corner of the Web. I'm a senior computer scientist interested in all scientific aspects of computer programming. I'm a professor at Collège de France, where I hold the chair of software sciences, and a member of Académie des sciences. I'm also a member of the Cambium research team of Inria. News [01/2024] Award: the 2023 ACM SIGPLAN Programming Languages Software Award was
ICFP 2010 実況など
kinaba @kinaba #WMM Appelの招待講演：静的解析器で不変条件を挿入→（以下Coqで）検証→公理的意味論から操作的意味論から双模倣で証明しやすい操作的意味論からLeroyのCompCertで抽象マシン語にコンパイルしてからPPCへ、という、並列性を扱えるCコンパイラツールチェインについて。 2010-09-25 23:39:52 kinaba @kinaba #WMM システムコールやpthreadはオラクルとして抽象化してやる。"この量の証明は機械化証明なしでは無理"、"証明のモジュール化(module,依存型,型クラス)重要"/(感想)それでもまだモジュール化機構が"足りてない"感を感じるけど証明言語は将来どうなるかなー 2010-09-25 23:50:59
高階関数クイズ - camlspotter’s blog
ちょっとした高階関数を使ったパズルです。前の会社の面接で使おうかなあと思っていたのですが、使う機会もなくなったので。全く別の機会に、高階関数を教えるための例を書いていて、遊んでいたら面白いものを見つけたので覚えていたのです。 # let twice f x = f (f x) これは f という関数と値 x をもらって、f を二回 x に適用する関数です。 次の add1 は引数 x を受け取って、１足して返す関数です。これを twice に使うと、こうなります。 # let add1 x = x + 1 # add1 0 1 # twice add1 0 2 関数型言語に慣れている方なら、twice ((+) 1) 0 でも同じですね。(OCaml を使っていますが、慣れていない方の為に、出力を一部省略しています。# はプロンプトです。コメントじゃありません。あと、入力の後には ;; を
ICFP Programming Contest 2010 終了 - まめめも
ref: http://icfpcontest.org/ 今回の課題は近年稀に見る面白さでした。要約するとこんな課題。 車とその燃料を開発して、市場に投入せよ。 市場に投入された車の設計書は参加者全員に公開される。燃料の設計書は公開されない。 他社の車の設計書を解析して、他社の車用の燃料を開発し市場に投入することもできる。売上はほぼ折半 *1 。 燃料の売上を競う。 以上より目的は、「解析が難しい車を設計して投入し、燃料の売上を寡占する」かつ「他人の車を解析して燃料を作り、売上を奪う」ということになります。すばらしい皮肉的な設定。 さらに ICFPC らしさとして、 車や燃料の設計書は trit 文字列 (0 と 1 と 2 のみからなる文字列) で書かれる。trit 文字列の仕様は非公開。適当に作った設計書を投入してみて、パースエラーのメッセージを元に、トライアンドエラーでフォーマットを
Ruby でパターンマッチ - まめめも
ref: 未来の国のアリス - d.y.d. で紹介されている implicit future が Ruby に欲しい！ # promise を作る x = Promise.new a = [1, x, 2, x, 3, x] # 今はまだ値になっていない p a #=> [1, _promise_, 2, _promise_, 3, _promise_] # この promise は 42 に決めた！ (代入ではないよ) x === 42 # x の箇所は勝手に 42 になっている p a #=> [1, 42, 2, 42, 3, 42] というのも、これがあれば Ruby でパターンマッチができる気がするんですよね。こんな感じに。 # 何にでもマッチする箇所には _ と書く (実体は Promise.new) def _ Promise.new end # + と定数だけからなる抽象
3imp 写経の日々その２(マニアむけ) - 言語ゲーム
というわけでやっと 4.7 章まで読み終えた感想です。 3imp は特に Lisp 系言語の利点を最大限に発揮した構成になっています。この限られたスペースの中で、コンパイラの実装について不足なく説明しきる事が出来た勝因は S 式とマクロでしょう。私は正直 S 式もマクロも嫌いですが、ことプログラミング言語の実装を解説するという用途において Lisp は最強という感想を持ちました。 まず S 式について。S 式を使うとパーサが不要です。世の中に出回っているコンパイラの教科書のかなりのスペースがパーサの説明になっている事を考えると、パーサが不要というのは画期的です。パーサの説明を省く事によっていきなり本質的な議論が出来るからです。 それからマクロについて。3imp のソースは SICP に比べて相当分かりやすいですが、その理由は record-case マクロによるパターンマッチもどきにあると
full abstraction - keigoiの日記
full abstraction ... λ計算とかπ計算とか表示的意味論のお話ではよく出てくる概念なんですが、未だによくわからないなーとつぶやいていたら id:sumii さんに教えていただいた。 もったいないのでここに残しておきます。 full abstraction の私的な説明 計算体系Aと計算体系(もしくはモデル)B があるとして、 その間の変換を C[・] : A -> B、 〜A と 〜B をそれぞれの計算体系(かモデル)における等価性とします。 すべてのAの項 ta1とta2について C[ta1] 〜B C[ta2] ならば ta1〜A ta2 ... adequacy(soundness) ta1 〜A ta2 ならば C[ta1] 〜B C[ta2] ... completeness この両方が成り立つとき、 変換は fully abstract であるといいます。 た
The Typeclassopediaを訳しました, The Typeclassopedia - #3(2009-10-20)
■ [Haskell] The Typeclassopediaを訳しました The Monad.ReaderのIssue 13に掲載されたThe Typeclassopediaという記事が、Functor, Monad, Monoid, Applicative, Foldable, Traversable, Arrowといったような型クラスについて良くまとまっていて、そのあたりを知りたい時の取っ掛かりになりそうだったので翻訳してみました。 作者のBrent Yorgeyさんからも許可がいただけたので公開します。翻訳に慣れていないので変な日本語（特に専門用語の日本語訳はかなり怪しい）があったり、そもそも間違っていたりするかもしれませんので、何か見つけたらコメントを頂けると助かります。 ■ [Haskell] The Typeclassopedia by Brent Yorgey <first
Route 477 - gemcutterの使い方まとめ (2009年秋)
■ [haskell] モナドって結局なんなの 社内勉強会でモナドについて発表しました。分かった気がするたびにすぐに手からすりぬけてしまう、それがモナド…！ 追記： モナドそのものが何なのかとか考えないほうがいいんじゃないですかね！ [Twitter / いーぐるとまとより引用] まさにその通りだと思います(笑)。IOの使い方、Maybeの使い方、Stateの使い方などを押さえておけば、 中がどうなってるかなんて知らなくても大丈夫。 でも、モナドの持つ「なんか秘技がありそうな感じ」が、中を覗いてみたくさせるんですよね。 この、どこまで掘っても自分の知らないことが出てくる感じがHaskellの魅力なのかも。 Haskell の本当にすごいところは、「なぜなに」を問いかけることでいつまでもプログラマが成長できるところにある。 [ふぁぼったー / ikegami__より引用] 一問一答 Q. モ
はじめてのにき(2009-10-14)
_ 検索がうまくないという話 なにか僕は絶望的にヘタな検索をするという話をよくする。 けど具体的にどんなヘタ検索だったか覚えてなかったので、 適当にログをあさってヘタそうな検索失敗例を探してきた。 たいてい単語が足りてなくて増やすのだけど、 増やす前の検索キーワードで目的のものが見つかるはずがない。 DS => カルドセプト DS MT => MT mersenne 永田 => 永田 赤軍 span => span style => span style height NTT => NTT goo あとは何が知りたかったのか見当もつかないようなクエリが たまにあるはず…と思ったのだけど、意外となかった。 不意に「はらへった」とかで検索してた気がするんだけどなぁ。 本気で意図がわからなかったのは、 「財布」「店主」などがあった。 「雪歩shinh」というのもあったが俺は一体何を期待していたの
Matzにっき(2008-02-01)
<< 2008/02/ 1 1. [言語] 「ハッカーと画家」の著者が新しいLisp系言語「Arc」を公開 | エンタープライズ | マイコミジャーナル 2. 「セキュリティ、なめんなよ!」 なめねこも一緒に情報セキュリティ強化宣言 | ネット | マイコミジャーナル 3. 「サイオステクノロジーはグルージェントの未来技術に期待し子会社化」：ITpro 2 1. [Ruby] Nimble Method: Garbage Collection is Why Ruby on Rails is Slow: Patches to Improve Performance 5x; Memory Profiling 2. [言語] LuaJIT roadmap 2008 3. [Ruby] What will Matz do? 4. [Ruby] EURUKO 2008 − European Ruby
Pythonのlambda - 西尾泰和のはてなダイアリー
プログラミングシンポジウムで言語パターン - 使いやすい言語・ライブラリをデザインする方法 - qwik.jp/lang-patternの発表を聞いていて、使ってほしくない機能は使いにくくするという話のところで「Pythonのlambdaが使いやすく改善されないのはGuidoが使ってほしくないと思っているから」と発言したらソースを求められたので調べてみた The fate of reduce() in Python 3000 Why drop lambda? Most Python users are unfamiliar with Lisp or Scheme, so the name is confusing; also, there is a widespread misunderstanding that lambda can do things that a nested fun
Route 477(2009-07-28)
■ [book][lisp] Let Over Lambdaを読んでCommon Lispに興味を持った 途中まで読んだ。 4434133632 Lispマクロを使っていろいろ遊ぶぜ！という本。内容は濃いけど、章(テーマ)が7つあり、一つ一つの節は短めなので少しずつ読んでいくことができる。 Lisp方言には「Common Lisp」と「Scheme」(あとArcとかClojureとか)があるわけだけど、 本書で「Lisp」と書いてあればCommon Lispの方を指す。だからLispコンパイラの存在は当然だし、リーダーマクロもある。 第3のアンクオート「,.」とか全く知らなかったぜ。 んでまあ、マクロと関係ないんだけど、Schemeはシンプルさを取るために、Lispが持っていたいろいろなものを切り捨ててるんだなぁというのを今さら。 loopマクロとか、「Common Lisp使いの書くLi
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
https://dl.acm.org/citation.cfm?doid=1806689.1806757
anarchy proof -
mamememo
Buzz by DeWitt Clinton from Buzz
NameBright - Coming Soon
The Kawa language framework
Archives of the Caml mailing list > Message from Jacques Garrigue