{{ message }}

Instantly share code, notes, and snippets.

🍣
SUSHI

# pandaman pandaman64

🍣
SUSHI
Last active Sep 6, 2020
View pointers_in_Paleolithic_age.md

# 概要

• ポインタは単なるアドレスではありません．
• ポインタにはprovenanceという，どのオブジェクト由来かの情報が含まれています．
Created Aug 30, 2020
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 Aug 25, 2020
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 Jun 7, 2020
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
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
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 Mar 20, 2020
View propagators.md

# Propagators

## 👀The Art of the Propagator

• Schemeかー
• bottomが無情報，topが矛盾なjoin semi-latticeと読めばよさそう
• ekmett的
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
• 最適化したい
• 例:
Last active Jul 5, 2018 — 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 Jul 2, 2018
View qft.ipynb