152
click to vote
AFP
2015
Springer
9 years 11 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 ...
118
Voted
AFP
2015
Springer
9 years 11 months ago
2015
Springer
Among the various mathematical tools introduced in his outstanding work on Communicating Sequential Processes, Hoare has defined ”interleaves” as the predicate satisfied by ...
132
click to vote
AFP
2015
Springer
9 years 11 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...
124
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
We provide a framework for registering automatic methods to derive class instances of datatypes, as it is possible using Haskell’s “deriving Ord, Show, . . . ” feature. We f...
132
Voted
AFP
2015
Springer
9 years 11 months ago
2015
Springer
The definition of noninterference security for Communicating Sequential Processes requires to consider any possible future, i.e. any indefinitely long sequence of subsequent eve...
125
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
We analyze the amortized complexity of dynamic tables with arbitrary minimal and maximal load factors and arbitrary expansion and contraction factors.
121
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
Euler’s Partition Theorem states that the number of partitions with only distinct parts is equal to the number of partitions with only odd parts. The combinatorial proof follows...
128
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
The classical definition of noninterference security for a deterministic state machine with outputs requires to consider the outputs produced by machine actions after any trace, ...
112
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
Isabelle/Isar provides named cases to structure proofs. This article contains an implementation of a proof method casify, which can be used to easily extend proof tools with suppo...
122
click to vote
AFP
2015
Springer
9 years 11 months ago
2015
Springer
This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides im...