Instantly share code, notes, and snippets.

🍣
SUSHI

# pandaman pandaman64

🍣
SUSHI
Last active September 6, 2020 13:29
View pointers_in_Paleolithic_age.md

# 概要

• ポインタは単なるアドレスではありません．
• ポインタにはprovenanceという，どのオブジェクト由来かの情報が含まれています．
Created August 30, 2020 07:25
View Euclid.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Created August 25, 2020 05:25
coprime
View Scratch.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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}"
Created June 7, 2020 21:53
View Derivative.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theory Pumping imports Main begin datatype 't regexp = EmptySet | EmptyStr | Char 't | App "'t regexp" "'t regexp" | Union "'t regexp" "'t regexp"
Created May 27, 2020 14:06
View Pumping.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 Theory Pumping (Isabelle2020: April 2020)

Theory Pumping

Last active May 27, 2020 14:08
View Pumping.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 theory Pumping imports Main begin datatype 't regexp = EmptySet | EmptyStr | Char 't | App "'t regexp" "'t regexp" | Union "'t regexp" "'t regexp"
Last active March 20, 2020 06:37
View propagators.md

# Propagators

## 👀The Art of the Propagator

• Schemeかー
• bottomが無情報，topが矛盾なjoin semi-latticeと読めばよさそう
• ekmett的
Last active December 18, 2020 07:54
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
• 最適化したい
• 例:
Last active July 5, 2018 11:41 — forked from fulmicoton/gist:b3637832363203f96740814119ad5a6c
View gist:eae733625851e3ce33f2780287be72f0
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
Created July 2, 2018 16:51
View qft.ipynb