keigoi

(* Proving soundness of STLC using autosubst https://www.ps.uni-saarland.de/autosubst/ *)

Require Import Autosubst MMap.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* our type - only booleans and functions *)

kaosf

sudo apt-get install haskell-platform
mkdir -p some/where/as/you/like
cd some/where/as/you/like
cabal install cabal-install
export PATH=$HOME/.cabal/bin:$PATH
cabal sandbox init
git clone git@github.com:pasberth/paradocs.git
cabal install ./paradocs
./.cabal-sandbox/bin/paradocs ./paradocs/doc/cheatsheet.pdoc > cheatsheet.html

mizchi

Atomコードリーディングメモ

ビルド方法

script/build

起動したらsrc/window-bootstrap.coffeeが起動時間のログを出してるので、そいつをgrepすると/src/broweser/atom-application.coffee が引っかかる。

src/broweser/atom-application.coffee は、 src/browser/main.coffee に呼ばれている

mala

概要

http://co3k.org/blog/csrf-token-should-not-be-session-id について。

この記事では触れられていませんが、

• むかし、セッションIDをHTMLソース中に埋め込んでも脅威は変わらないと主張した人がいました
• 正確には「hiddenの値のみ漏れやすいような特殊な脆弱性が無ければ」という前提であったけれど、実際にそのようなバグはあったし、予見されていた。
• とても影響のある人だったので、色々なサイトや書籍がその方法を紹介し、安全なウェブサイトの作り方にも載ってしまいました

この際ハッキリ言っておくべきだと思うので書きますが、そもそもセッションIDを(HTMLソース中に埋め込む)CSRF対策トークンとして使うのは間違いでした。最初から間違っていたのです。正確に言うとCSRFの話は関係ないですね。CSRF関係なく、特に「単体で」セッションハイジャックが可能になるような値を、HTMLソース中に埋め込むべきではありません。

yutopp

// 2013/12/25
def main(): void
{
    val i = 0: int mutable;
    while( i < 10 ) {
        pl( i );
        i = i + 1;
    }
    print( "   #rill  || #xmas\n" );
}

mathink

(* HORS? *)

Set Implicit Arguments.
Require Import List.

CoInductive List (A: Set): Set :=
| Nil | Cons (head: A)(tail: List A).
Arguments Nil {A}.
Arguments Cons {A}(head)(tail).

mathink

Require Import 
        Ssreflect.ssreflect Ssreflect.ssrbool Ssreflect.ssrfun
        Ssreflect.ssrnat Ssreflect.prime Ssreflect.seq
        Ssreflect.div Ssreflect.binomial Ssreflect.bigop.

Lemma coprime_plus a b:
  coprime a (b+a) -> coprime b (b+a).
Proof.
  by rewrite /coprime gcdnDl gcdnDr gcdnC.
Qed.  

cosmo0920

% ./dist/build/test-aeson-lens/test-aeson-lens
"127.0.0.1"
"27017"

myuon

{-# LANGUAGE TemplateHaskell, FlexibleContexts, FlexibleInstances, UndecidableInstances, OverlappingInstances #-}
import Control.Lens
import Control.Monad.State

-- 基本となるオブジェクト
data Obj = Obj {
  _pos :: Int
  } deriving (Show)

-- Obj型のオブジェクトをもつ抽象的なクラスHasObjを作る

halcat0x15a

Pipeモナドの紹介

Scalaの記事です。Haskellはあまり書けません。

Iterateeの複雑さから開放されたいのでPipe系ライブラリ使いましょうという記事です。

Iterateeとの比較や簡単な使い方についてつらつらと書いていきます。

Iterateeについて