Skip to content

Instantly share code, notes, and snippets.

View pandaman64's full-sized avatar
🍣
SUSHI

pandaman pandaman64

🍣
SUSHI
49 followers · 14 following
View GitHub Profile
@pandaman64
pandaman64 / pointers_in_Paleolithic_age.md
Last active September 6, 2020 13:29

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

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

概要

  • ポインタは単なるアドレスではありません．
  • ポインタにはprovenanceという，どのオブジェクト由来かの情報が含まれています．
@pandaman64
pandaman64 / Euclid.thy
Created August 30, 2020 07:25
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
@pandaman64
pandaman64 / Scratch.thy
Created August 25, 2020 05:25
coprime
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}"
@pandaman64
pandaman64 / Derivative.thy
Created June 7, 2020 21:53
theory Pumping
imports Main
begin
datatype 't regexp =
EmptySet
| EmptyStr
| Char 't
| App "'t regexp" "'t regexp"
| Union "'t regexp" "'t regexp"
@pandaman64
pandaman64 / Pumping.html
Created May 27, 2020 14:06
<!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>
@pandaman64
pandaman64 / Pumping.thy
Last active May 27, 2020 14:08
theory Pumping
imports Main
begin
datatype 't regexp =
EmptySet
| EmptyStr
| Char 't
| App "'t regexp" "'t regexp"
| Union "'t regexp" "'t regexp"
@pandaman64
pandaman64 / propagators.md
Last active March 20, 2020 06:37

Propagators

👀The Art of the Propagator

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

色々メモリモデル

コンパイラ（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
      • 最適化したい
  • 例:
@pandaman64
pandaman64 / gist:eae733625851e3ce33f2780287be72f0
Last active July 5, 2018 11:41 — forked from fulmicoton/gist:b3637832363203f96740814119ad5a6c
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
@pandaman64
pandaman64 / qft.ipynb
Created July 2, 2018 16:51
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.