--- a/src/parallel_execution/stack.agda	Tue Nov 15 19:02:36 2016 +0900
+++ b/src/parallel_execution/stack.agda	Tue Nov 15 19:33:13 2016 +0900
@@ -1,13 +1,34 @@
 module stack where
 
-pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
+record Stack {a : Set} (stackImpl : Set a) where
+  stack : stackImpl
+  push : stackImpl -> a -> (stackImpl -> T) -> T
+  pop  : stackImpl -> (stackImpl -> maybe a -> T) -> T
+  
+
+createSingleLinkedStack : Stack (SingleLinkedStack {a})
+createSingleLinkedStack = record { 
+  stack = record { top = nothing;}
+  push  = pushSingleLinkedStack;
+  pop   = popSingleLinkedStack;
+}
+
+
+record Element {a : Set} : Set where
+  data : a
+  next : Maybe (Element a)
+
+record SingleLinkedStack {a : Set} : Set where
+  top : Maybe (Element a)
+
+pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
 pushSingleLinkedStack stack data next = next stack1
   where
     element = record {next = top stack; data = data}
     stack1  = record {top = just element}
 
 
-popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
+popSingleLinkedStack : {a : Set} -> Maybe a -> Data -> (Code : Stack -> (Maybe a) -> T) -> T
 popSingleLinkedStack stack data next with (top stack) =
   ... | nothing = next stack nothing
   ... | just a  = next stack1 data1