Skip to content

Instantly share code, notes, and snippets.

🍣
SUSHI

pandaman pandaman64

🍣
SUSHI
View GitHub Profile
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 May 6, 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
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
View config.nix
with (import <nixpkgs> {});
{
allowUnfree = true;
packageOverrides = pkgs: with pkgs; {
userPackages = buildEnv {
inherit ((import <nixpkgs/nixos> {}).config.system.path)
pathsToLink ignoreCollisions postBuild;
extraOutputsToInstall = [ "man" ];
name = "user-packages";
paths = [
View .vimrc
if &compatible
set nocompatible
endif
set runtimepath+=/home/pan/.vim/bundles/repos/github.com/Shougo/dein.vim
if dein#load_state('/home/pan/.vim/bundles')
call dein#begin('/home/pan/.vim/bundles')
call dein#add('/home/pan/.vim/bundles/repos/github.com/Shougo/dein.vim')
View .vimrc
if &compatible
set nocompatible
endif
set runtimepath+=/home/pan/.vim/bundles/repos/github.com/Shougo/dein.vim
if dein#load_state('/home/pan/.vim/bundles')
call dein#begin('/home/pan/.vim/bundles')
call dein#add('/home/pan/.vim/bundles/repos/github.com/Shougo/dein.vim')
You can’t perform that action at this time.