Sciweavers

Share
AFP
2015
Springer
3 years 8 months ago
Derivatives of Logical Formulas
We formalize new decision procedures for WS1S, M2L(Str), and Presburger Arithmetics. Formulas of these logics denote regular languages. Unlike traditional decision procedures, we ...
Dmitriy Traytel
AFP
2015
Springer
3 years 8 months ago
Descartes' Rule of Signs
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. ...
Manuel Eberl
AFP
2015
Springer
3 years 8 months ago
The Inductive Unwinding Theorem for CSP Noninterference Security
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 ...
Pasquale Noce
AFP
2015
Springer
3 years 8 months ago
Reasoning about Lists via List Interleaving
Among the various mathematical tools introduced in his outstanding work on Communicating Sequential Processes, Hoare has defined ”interleaves” as the predicate satisfied by ...
Pasquale Noce
AFP
2015
Springer
3 years 8 months ago
Applicative Lifting
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...
Andreas Lochbihler, Joshua Schneider
AFP
2015
Springer
3 years 8 months ago
Deriving class instances for datatypes
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...
Christian Sternagel, René Thiemann
AFP
2015
Springer
3 years 8 months ago
The Ipurge Unwinding Theorem for CSP Noninterference Security
The definition of noninterference security for Communicating Sequential Processes requires to consider any possible future, i.e. any indefinitely long sequence of subsequent eve...
Pasquale Noce
AFP
2015
Springer
3 years 8 months ago
Parameterized Dynamic Tables
We analyze the amortized complexity of dynamic tables with arbitrary minimal and maximal load factors and arbitrary expansion and contraction factors.
Tobias Nipkow
AFP
2015
Springer
3 years 8 months ago
Euler's Partition Theorem
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...
Lukas Bulwahn
AFP
2015
Springer
3 years 8 months ago
The Generic Unwinding Theorem for CSP Noninterference Security
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, ...
Pasquale Noce
books