PiDuce
Summary for paper "A basic contract language for web services"
The authors have proposed a schema language to describe webservices. The essence is similar to CDuce's type with the following relation on channels.
<R>i means a channel receives R as input.
<R>o means a channel produces R as output.
<R>io means a channel receives and produces R.
So <R>i = R -> _|_, <R>o = Any -> R and <R>io= R -> R
The problem defined in this paper is that validating a webservice request (a value) w.r.t to the schema happens at run time. Because channel does not carry structural information but type annotation, subtyping check must be performed at run time, which is EXP.
The solution is to reconsider a subset of regular hedges, the rough idea is to disallow A*,A*. If we normalize it, we get A,A*,A*| A,A* | (), since the first two monomails shares the same leading literal, with antimirov's algorithm we would combine the two. But this leads to exponential blow up the size of the proof. It is worse if regular hedge is considered. So the authors decided to disallow this kind of type. Assume the subset should be deterministic by normalization without combining and monomials. (Though this is my rough understanding.)
TODO: check whether their definition is complete!!!
They have a nice result showing that considering this subset of type, would produce an efficient proving algorithm in polynormial time.
The authors have proposed a schema language to describe webservices. The essence is similar to CDuce's type with the following relation on channels.
<R>i means a channel receives R as input.
<R>o means a channel produces R as output.
<R>io means a channel receives and produces R.
So <R>i = R -> _|_, <R>o = Any -> R and <R>io= R -> R
The problem defined in this paper is that validating a webservice request (a value) w.r.t to the schema happens at run time. Because channel does not carry structural information but type annotation, subtyping check must be performed at run time, which is EXP.
The solution is to reconsider a subset of regular hedges, the rough idea is to disallow A*,A*. If we normalize it, we get A,A*,A*| A,A* | (), since the first two monomails shares the same leading literal, with antimirov's algorithm we would combine the two. But this leads to exponential blow up the size of the proof. It is worse if regular hedge is considered. So the authors decided to disallow this kind of type. Assume the subset should be deterministic by normalization without combining and monomials. (Though this is my rough understanding.)
TODO: check whether their definition is complete!!!
They have a nice result showing that considering this subset of type, would produce an efficient proving algorithm in polynormial time.
