Pointers Are Complicated II, or: We need better language specs
Pointers Are Complicated II, or: We need better language specs Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that just because two pointers point to the same address, does not mean they are equal in the sense that they can be used interchangeably. This “extra information” that distinguishes different pointers to the
Semantic Versioningの闇 - knqyf263's blog
今回も誰も興味ないシリーズなので今まで書いてこなかったのですが、Semantic Versioningに関して幻想を抱いている人がいる可能性があり、そういう方にどうしても現実を知っておいて欲しかったので書きました。3行要約（と可能なら余談）だけでも読んでいただけると幸いです。 3行要約 Semantic Versioning 2.0.0にはバージョン"比較"の定義はあるが、バージョン"制約"（>= 2.1.3みたいなやつ）の定義がない その結果、同じsemver準拠ライブラリでも制約の解釈が異なり結果が真逆になる というかそもそもsemver使ってるエコシステムが少なすぎる 背景 セキュリティアドバイザリでは特定のバージョンが脆弱であることを示すためにバージョン制約が使われることが多いです。例えば >=1.2.0 <1.2.6みたいなやつです。この場合、1.2.5は脆弱だが1.2.6は修正
People of Programming Languages
People of Programming Languages An interview project in conjunction with POPL 2018 Simon Peyton-Jones Simon Peyton-Jones (Microsoft Research Cambridge), one of the key people behind the development of Haskell, talks about seeing functional programming go from intellectual revolution to practical reality and the importance of investing in computing education. Hongseok Yang Hongseok Yang is a Profes
CompCert - Main page
The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees
再帰プログラムの意味論について
∗ 1 semantics of programming languages recursion ∗ 59 (2007), 180–191 1 2 2.1 fact(x) ≡ if x = 0 then 1 else x × fact(x−1) well-defined Z * Z Z * Z F : (Z * Z) → (Z * Z) F(f)(x) = 1 (x = 0) x × f(x − 1) (x 6= 0, f(x − 1) ) ( ) F F fact fact [[fact]] : Z * Z [[fact]](x) = ( x! (x ≥ 0) ( ) 2 F f [[fact]] F([[fact]])(x) = 1 (x = 0) x × y (x 6= 0, [[fact]](x−1) = y) ( ) = ( x! (x ≥
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Imperative Programs as Proofs via Game Semantics | Lambda the Ultimate
