Skip to content

Instantly share code, notes, and snippets.

View kik's full-sized avatar

kik kik

27 followers · 1 following
View GitHub Profile
@kik
kik / README
Created June 6, 2014 15:42
TLS in Coq
ちょっとだけ脳内ダンプしたコードがあった
こんな感じにTLSEngineの内部には6個のバッファーがあって、状態遷移は基本的にどっかのバッファーの先頭から取ってきて、
加工した結果をどっかのバッファーの末尾に置くって感じで書く予定だった。
CCSがソケット入力バッファーの先頭にあるときに、ハンドシェークの状態が特定の状態にないといけないのは自明のことで、
本当の興味は他のバッファーの状態がどうなってないといけないのか？ということだったんだー
@kik
kik / test
Created December 14, 2013 19:15
test
<!DOCTYPE html>
<html>
<head>
<title>Bootstrap 101 Template</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<!-- Bootstrap -->
<link href="css/bootstrap.min.css" rel="stylesheet">
<!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
<!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
@kik
kik / ToyPr.hs
Last active December 25, 2015 23:09
おもちゃ証明器 僕の証明器はEckmann-Hiltonの定理が証明できる！2次のホモトピー群は可換群だ！ Proof term は全然読めなくなってきた。
{-# LANGUAGE TupleSections #-}
import Data.List
import Data.Maybe
import Data.IORef
import Control.Applicative
import Control.Exception hiding (try, assert)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Error
@kik
kik / HoTT2.hs
Created October 13, 2013 18:03
型検査は足りてないけど、PHOASやめてdeBruinインデックスに変えた。PHOASみたいにキチガイじみた難しさはないぽ
-- {-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}
-- import Control.Monad.Reader
data Term = TmU Int
| TmVar Int
| TmProd Type Term
@kik
kik / LC.hs
Last active December 23, 2015 22:19
ラムダ計算をHaskellで書いてる途中。自由変数がいくつあるかを型に埋め込みたいと思った。やっぱりGADTにした。
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- {-# LANGUAGE StandaloneDeriving #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}
import Control.Monad.Reader hiding (join)
data TermP v where
@kik
kik / HoTT.hs
Created September 23, 2013 14:12
型検査は足りてないけど、型検査が通った場合に返ってくる型は返せるようになった！
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE StandaloneDeriving #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}
import Control.Monad.Reader hiding (join)
data TermP v where
TmFamily :: TermP v -> (v -> TermP v) -> TermP v
@kik
kik / STLC.hs
Last active December 23, 2015 15:49
項が複製される場所を減らした。そのかわり気持ち悪い関数が発生した。これどうにもならんもんなん？
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}
import Control.Monad.Reader
data Typ where
TBool :: Typ
TArrow :: Typ -> Typ -> Typ
@kik
kik / STLC.hs
Created September 21, 2013 20:15
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
import Control.Monad.Reader
data Typ where
TBool :: Typ
TArrow :: Typ -> Typ -> Typ
deriving (Show, Eq)
@kik
kik / SLC.hs
Created September 21, 2013 15:35
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
import Control.Monad.Reader
data Typ t where
TBool :: Typ Bool
TArrow :: Typ a -> Typ b -> Typ (a -> b)
@kik
kik / gist:6209891
Created August 12, 2013 10:55
ICFPC 2013 最終コード
#include <unistd.h>
#include <cstdlib>
#include <cstdio>
#include <vector>
#include <iostream>
#include <utility>
#include <string>
#include <random>
#include <memory>