Skip to content

Instantly share code, notes, and snippets.

View pointers_in_Paleolithic_age.md

旧石器時代のポインタをご利用の皆様へ ~provenance入門~

現代のプログラミング言語ではポインタは単なるアドレスではなく,provenanceを伴った参照として扱われています. 知識をアップデートしましょう.

概要

  • ポインタは単なるアドレスではありません.
  • ポインタにはprovenanceという,どのオブジェクト由来かの情報が含まれています.
View Euclid.thy
theory Euclid
imports Main "HOL-Library.Disjoint_Sets"
begin
fun prime :: "nat ⇒ bool" where
"prime n ⟷ n ≥ 2 ∧ (∀k ≤ n. k dvd n ⟶ k = 1 ∨ k = n)"
lemma "prime 5"
by code_simp
View Scratch.thy
theory Scratch
imports Main
begin
lemma
fixes m n
assumes "m ≥ 2" "n ≥ 2"
shows "coprime m n ⟷ (∃a b. a * int m + b * int n = 1)"
proof
let ?A = "{1..n}"
View Derivative.thy
theory Pumping
imports Main
begin
datatype 't regexp =
EmptySet
| EmptyStr
| Char 't
| App "'t regexp" "'t regexp"
| Union "'t regexp" "'t regexp"
View Pumping.html
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<title>Theory Pumping (Isabelle2020: April 2020)</title>
<link media="all" rel="stylesheet" type="text/css" href="isabelle.css"/>
</head>
<body>
<div class="head"><h1>Theory Pumping</h1>
View Pumping.thy
theory Pumping
imports Main
begin
datatype 't regexp =
EmptySet
| EmptyStr
| Char 't
| App "'t regexp" "'t regexp"
| Union "'t regexp" "'t regexp"
View propagators.md

Propagators

👀The Art of the Propagator

  • Schemeかー
  • bottomが無情報,topが矛盾なjoin semi-latticeと読めばよさそう
    • ekmett的
@pandaman64
pandaman64 / memory_model.md
Last active Dec 18, 2020
papers on formalized memory models
View memory_model.md

色々メモリモデル

コンパイラ(LLVM)のメモリモデル

Reconclining high-level optimization and low-level code in LLVM (https://dl.acm.org/doi/10.1145/3276495)

Lee, Hur, Jung, Liu, Regehr, Lopes.

  • 低レベル言語(C, C++, Rust)のコンパイラのメモリモデルには二つの相反する目標がある
    • high-level optimization
      • 最適化したい
      • 例:
View gist:eae733625851e3ce33f2780287be72f0
Let's call (r_i)_{i>=0} the sequence of the ranks of (A^i)_{i>=0}.
For any i>=0, the image of A^{i+1} is a subspace of the image of A^{i}.
Our sequence of ranks (r_i) is non-increasing.
Since Im(A^{i+1}) ⊂ Im(A^i), if there exists i such that r_i = r_{i+1}, Im(A^{i+1}) = Im(A^i).
From this, it follows that Im(A^k) = Im(A^i) (k > i), or r_k = r_i.
In other words, (r_i) is a sequence of non-negative integers that
- starts at n
- might be stricly decreasing for a while
View qft.ipynb
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.