105
click to vote
AFP
2015
Springer
9 years 9 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...
108
click to vote
AFP
2015
Springer
9 years 9 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, ...
AFP
2015
Springer
9 years 9 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...
105
click to vote
AFP
2015
Springer
9 years 9 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...
101
click to vote
AFP
2015
Springer
9 years 9 months ago
2015
Springer
Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are...
112
click to vote
AFP
2015
Springer
9 years 9 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...
102
click to vote
AFP
2015
Springer
9 years 9 months ago
2015
Springer
In this work, we prove the lower bound ln(Hn)−ln(5 3 ) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series n p=1[p p...
109
click to vote
AFP
2015
Springer
9 years 9 months ago
2015
Springer
Based on existing libraries for matrices, factorization of rational polynomials, and Sturm’s theorem, we formalized algebraic numbers in Isabelle/HOL. Our development serves as ...
AF
2015
9 years 9 months ago
2015
We present a new method to measure the intraday relationship between movements of implied volatility smiles and stock returns. It is based on an enhanced smile regression model wh...