130
click to vote
AFP
9 years 8 months ago
2015 Springer 
The necessary and sufficient condition for CSP noninterference security stated by the Ipurge Unwinding Theorem is expressed in terms of a pair of event lists varying over the set ...
115
click to vote
AFP
9 years 8 months ago
2015 Springer 
In this work, we formally proved Descartes Rule of Signs, which relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient list. ...
111
click to vote
AFP
9 years 8 months ago
2015 Springer 
Applicative functors augment computations with effects by lifting function application to types which model the effects [5]. As the structure of the computation cannot depend on...
104
click to vote
AFP
9 years 8 months ago
2015 Springer 
Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers...
|
Formal Methods