I have been reading the paper[1] in the title. But there are some parts of it that are unclear to me, more specifically the way you typecheck a lambda. I have attached the typing rules below as images[2] [3] Typing them all in Mathjax would have been a lot of work.I will explain the issue I am having by means of an example.Given the program in listing 1, we first apply the rule C-Let. This means that we typecheck the first binding, namely new !Int.End which yields the type [!Int.End].  $\Gamma$ now contains a mapping $x \rightarrow [!Int.End]$. Then we typecheck the next let, using C-Let once more. This time we typecheck accept x, which first makes sure that $x$ is of the proper type. $\Gamma$ contains this mapping so that is indeed the case. This yields the type Chan c. Note that when you look at the typing rule for accept, $c$ in this case is a so-called fresh variable. The rule C-Accept also inserts the session type into $\Sigma$. So $\Sigma$ contains a mapping $c \rightarrow\ !Int.End$ and $\Gamma$ contains two mappings, namely $\Gamma = x \rightarrow [!Int.End] , v \rightarrow Chan \ c$We then proceed to typecheck the last body of the most-inner let. The first statement is a send statement so we apply rule C-SendD. Typechecking the number $5$ yields type Int, so that part is correct. $v$ yields the type $Chan\ c$. $\Sigma$ indeed contains a mapping $c \rightarrow\ !Int.End$. So the rule C-SendD finally yields the type $\Sigma;Unit;c:End$ where the first part of the entry in $\Sigma$ has been consumed, leaving the session type for $c$ to $End$.Finally we can apply the rule C-Close which also typechecks properly.Listing 1let x = new !Int.End inlet v = accept x in  send 5 on v;  close v;We can now transform the above example to the following:Listing 2let x = new !Int.End inlet v = accept x inlet f = (Lambda x:Int . (close v))  send 5 on v;  (f 1);Listing 2 shows that instead of just calling close on the channel we have stored that operation inside a lambda. We will play typechecker one more.The first part of the typechecking is the same as above. So we have arrived at typechecking the body of the second let, namely let f =.... At this point $\Sigma = c \rightarrow\ !Int.End$ and $\Gamma = x \rightarrow [!Int.End] , v \rightarrow Chan \ c$.The body of the lambda uses a channel that is defined outside of the lambda, namely $v$. According to the paper, the required $\Sigma$ should be embedded in the type signature of the lambda. However, this is where things get unclear. If I follow the typing rules I would have written down the lambda as $(Lambda\ [c \rightarrow End,\ x:Int]\ .\ (close\ v))$. But this is impossible, I think.Recall that the rule C-Accept uses $fresh$ to generate a symbol that will be the identifier in $\Sigma$ and the second part of the type of the channel (e.g., $Chan\ c$). This means that it is impossible for the programmer to write down this identifier. Unless, of course, the channel is the parameter of the lambda itself. Then we can use $\alpha$-renaming. But this is not the case here, the channel is simply captured by the lambda and the parameter is $x$ which is ignored in the body of the lambda.So, there are two options the way I see it. The text in Listing 2 is illegal for the reason that you can not capture a channel that has not been passed to the lambda as a parameter. However, the paper shows an example of this at page 9. So this reasoning is probably faulty.The second reasoning I can come up with is the following. At the time the lambda is typechecked (as the binding to $f$), the typechecker will error because we are calling close on a channel that has session type $!Int.End$ in $\Sigma$. But, this could then be resolved by delaying the typechecking of the lambda until the point that it is invoked. But then, this does not require the programmer to write down the $\Sigma$ in the type signature of the lambda.I hope the problem I have sketched here is clear. Any feedback is appreciated.[1] Paper discussed in this question
Question about Type checking a multithreaded functional language with session types by Vasconcelos et al
type checking
I think(Lambda [cEnd, x:Int] . (close v))is indeed what you need to write.  As you mention, it's impossible to write it because c is fresh.  From my reading of it, it does seem to be a problem in the paper.I don't think this is a very serious problem, tho, since the same problem appears in other systems and has known solutions (look at the papers about Calculus of Capabilities or Alias Types, for example).if, as you do in your own syntax, you rely on type-inference, the problem disappears: the type inference can write the c since by that time it is known.you can change accept and request to return two things: a type c and a value of type Chan C.  I.e. introduce channel type parameters.  Indeed Chan c is a singleton type, so you need c to be able to parameterize over c in order to be able to do anything useful.