keigoi

channel.cmi :
mVar.cmi :
monitor.cmi :
session.cmi :
channel.cmo : monitor.cmi channel.cmi
channel.cmx : monitor.cmx channel.cmi
example.cmo : session.cmi
example.cmx : session.cmx
mVar.cmo : monitor.cmi mVar.cmi
mVar.cmx : monitor.cmx mVar.cmi

keigoi

{-# LANGUAGE ScopedTypeVariables, KindSignatures #-}
import Data.Typeable

innerTypeOf :: Typeable a => t a -> TypeRep
innerTypeOf (x :: t a) = typeOf (undefined :: a) -- fail

-- giving a kind explicitly will do
-- innerTypeOf (x :: t (a:: *)) = typeOf (undefined :: a) -- ok

keigoi

// use tail-call only, but stack overflow occur
fn recur(i : int) {
  if i!=0 {
    recur(i-1);
  }
}

fn main() {
    recur(1000000);
}

keigoi

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, TypeOperators #-}
--
-- MVar without deadlock
--

module CheckMVar (Z(Z),S(S),(:<),Nil,ListPos,Get,Set,Session,sreturn,sbind,runSession,inSession,inS,FullMVar,EmptyMVar,newMVar,newEmptyMVar,takeMVar,putMVar) where

import qualified Control.Concurrent as C

-- | type level zero

keigoi

(* Coroutine implementation in OCaml, with Oleg's delimited continuation *)
(* see http://okmij.org/ftp/continuations/implementations.html#caml-shift *)
module D = Delimcc

(* Coroutine yielded a value of type 'a, and will resume with some value of type 'b *)
type ('a, 'b) suspend =
  | Cont of 'a * ('b, ('a,'b) suspend) D.subcont
  | Finish

let start_coroutine f = 

keigoi

{-# LANGUAGE GADTs, FlexibleInstances #-}


module Main where

import Control.Monad
import Control.Monad.RWS.Strict
import Control.Monad.Trans.Error
import Prelude hiding (putChar, getChar)
import qualified System.IO as IO

keigoi

Axiom A :Set.
CoInductive Stream := Cons : A -> Stream -> Stream.

Definition head (s:Stream) : A :=
   match s with
    Cons x _ => x
  end.

Definition tail (s:Stream) : Stream :=
  match s with

keigoi

(*
OCaml fails with SEGV instead of exception Stack_overflow
- by Keigo IMAI <keigo.imai@gmail.com>

ocamlopt -g -thread -I +threads unix.cmxa threads.cmxa segv_stackovfl.ml -o a.out
ulimit -s 8192
./a.out 540000
 *)

let rec run_forever x = 

keigoi

session.cmi :
example.cmo : session.cmi
example.cmx : session.cmx
session.cmo : session.cmi
session.cmx : session.cmi

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 *)