We introduce a formal framework for analyzing trades in financial markets. An
exchange is where multiple buyers and sellers participate to trade. These days,
all big exchanges use computer algorithms that implement double sided auctions
to match buy and sell requests and these algorithms must abide by certain
regulatory guidelines. For example, market regulators enforce that a matching
produced by exchanges should be \emph{fair}, \emph{uniform} and
\emph{individual rational}. To verify these properties of trades, we first
formally define these notions in a theorem prover and then give formal proofs
of relevant results on matchings. Finally, we use this framework to verify
properties of two important classes of double sided auctions. All the
definitions and results presented in this paper are completely formalised in
the Coq proof assistant without adding any additional axioms to it.

more |
pdf
| html
None.

Jose_A_Alonso:
Formal verification of trading in financial markets. https://t.co/CERD95nxjU #ITP #Coq

okateim:
2019/07/19 [9]
Formal verification of trading in financial markets (https://t.co/V3DX7odE26)

DO:
Formal verification of trading in financial markets. https://t.co/sbljZ0YDct

arxiv_cslo:
Formal verification of trading in financial markets https://t.co/UIATJyK3Gz

jpt401:
RT @Jose_A_Alonso: Formal verification of trading in financial markets. https://t.co/CERD95nxjU #ITP #Coq

urosn:
RT @Jose_A_Alonso: Formal verification of trading in financial markets. https://t.co/CERD95nxjU #ITP #Coq

None.

None.

Sample Sizes : None.

Authors: 2

Total Words: 0

Unqiue Words: 0

The usual homogeneous form of equality type in Martin-L\"of Type Theory
contains identifications between elements of the same type. By contrast, the
heterogeneous form of equality contains identifications between elements of
possibly different types. This paper introduces a simple set of axioms for such
types. The axioms are equivalent to the combination of systematic elimination
rules for both forms of equality, albeit with typal (also known as
"propositional") computation properties, together with Streicher's Axiom K, or
equivalently, the principle of uniqueness of identity proofs.

more |
pdf
| html
None.

arxiv_cslo:
Typal Heterogeneous Equality Types https://t.co/lxDsz8CEnT

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 4550

Unqiue Words: 1166

A quotient construction defines an abstract type from a concrete type, using
an equivalence relation to identify elements of the concrete type that are to
be regarded as indistinguishable. The elements of a quotient type are
\emph{equivalence classes}: sets of equivalent concrete values. Simple
techniques are presented for defining and reasoning about quotient
constructions, based on a general lemma library concerning functions that
operate on equivalence classes. The techniques are applied to a definition of
the integers from the natural numbers, and then to the definition of a
recursive datatype satisfying equational constraints.

more |
pdf
| html
None.

arxiv_cslo:
Defining Functions on Equivalence Classes https://t.co/Xo0OT1R4eP

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 7515

Unqiue Words: 2138

We present a new method for model-based mutation-driven test case generation.
Mutants are generated by making small syntactical modifications to the model or
source code of the system under test. A test case kills a mutant if the
behavior of the mutant deviates from the original system when running the test.
In this work, we use hyperproperties-which allow to express relations between
multiple executions-to formalize different notions of killing for both
deterministic as well as non-deterministic models. The resulting
hyperproperties are universal in the sense that they apply to arbitrary
reactive models and mutants. Moreover, an off-the-shelf model checking tool for
hyperproperties can be used to generate test cases. We evaluate our approach on
a number of models expressed in two different modeling languages by generating
tests using a state-of-the-art mutation testing tool.

more |
pdf
| html
None.

arxiv_cslo:
Mutation Testing with Hyperproperties https://t.co/EhIIdw9bZV

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 0

Unqiue Words: 0

There are multiple ways to formalise the metatheory of type theory. For some
purposes, it is enough to consider specific models of a type theory, but
sometimes it is necessary to refer to the syntax, for example in proofs of
canonicity and normalisation. One option is to embed the syntax deeply, by
using inductive definitions in a proof assistant. However, in this case the
handling of definitional equalities becomes technically challenging.
Alternatively, we can reuse conversion checking in the metatheory by shallowly
embedding the object theory. In this paper, we consider the standard model of a
type theoretic object theory in Agda. This model has the property that all of
its equalities hold definitionally, and we can use it as a shallow embedding by
building expressions from the components of this model. However, if we are to
reason soundly about the syntax with this setup, we must ensure that
distinguishable syntactic constructs do not become provably equal when
shallowly embedded. First, we prove that shallow embedding is...

more |
pdf
| html
None.

arxiv_cslo:
Shallow Embedding of Type Theory is Morally Correct https://t.co/uYz38A85v3

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 0

Unqiue Words: 0

The $tock$-CSP encoding embeds a rich and flexible approach to modelling
discrete timed behaviours in CSP where the event $tock$ is interpreted to mark
the passage of time. The model checker FDR provides tailored support for
$tock$-CSP, including a prioritisation operator that has typically been used to
ensure maximal progress, where time only advances after internal activity has
stabilised. Prioritisation may also be used on its own right as a modelling
construct. Its operational semantics, however, is only congruent over the most
discriminating semantic model of CSP: the finite-linear model. To enable sound
and compositional reasoning in a $tock$-CSP setting, we calculate a
denotational definition for prioritisation. For that we establish a Galois
connection between a specialisation of the finite-linear model, with $tock$ and
$\checkmark$, that signals termination, as special events, and
$\checkmark$-$tock$-CSP, a model for $tock$-CSP that captures termination,
deadlines, and is adequate for reasoning about timed refinement. Our...

more |
pdf
| html
None.

arxiv_cslo:
Priorities in tock-CSP https://t.co/HqOt7hiPEJ

None.

None.

Sample Sizes : None.

Authors: 3

Total Words: 7078

Unqiue Words: 1517

Runtime Verification (RV) studies how to analyze execution traces of a system
under observation. Stream Runtime Verification (SRV) applies stream
transformations to obtain information from observed traces. Incomplete traces
with information missing in gaps pose a common challenge when applying RV and
SRV techniques to real-world systems as RV approaches typically require the
complete trace without missing parts. This paper presents a solution to perform
SRV on incomplete traces based on abstraction. We use TeSSLa as specification
language for non-synchronized timed event streams and define abstract event
streams representing the set of all possible traces that could have occurred
during gaps in the input trace. We show how to translate a TeSSLa specification
to its abstract counterpart that can propagate gaps through the transformation
of the input streams and thus generate sound outputs even if the input streams
contain gaps and events with imprecise values. The solution has been
implemented as a set of macros for the original...

more |
pdf
| html
None.

arxiv_cslo:
Runtime Verification For Timed Event Streams With Partial Information https://t.co/IH4BH9F93V

None.

None.

Sample Sizes : None.

Authors: 5

Total Words: 0

Unqiue Words: 0

In paper describes the new logic programming language Delta, which have a
many good properties. Delta-programs is p-computable, verifiable and can
translation on other languages. Also we describe the Delta-methodology for
constructing p-computable programs in high-level languages such as PHP, Java,
JavaScript, C++, Pascal, Delphi, Python, Solidity and other. We would like to
especially note the use of the Delta methodology for creating Smart Contracts
and for Internet of things. We change the concept of the formula and define
D-formulas(or Delta programs) are special list-formulas. Then we define the
execution of a program how is the process of checking truth D-formula on a
dynamic model. Main idea our paper consider program how list-formula from
another formulas on dynamic models. And we created by iterations new
Delta-programs use simple base formulas for this. Also we entered a dynamic
models how models where we save final values of variables when check formula on
this model.

more |
pdf
| html
None.

arxiv_cslo:
Delta -- new logic programming language and Delta-methodology for p-computable programs on Turing Complete Languages https://t.co/SOsuzWhyQ9

None.

None.

Sample Sizes : None.

Authors: 1

Total Words: 0

Unqiue Words: 0

Assert is a website where the best academic papers on arXiv (computer science, math, physics), bioRxiv (biology), BITSS (reproducibility), EarthArXiv (earth science), engrXiv (engineering), LawArXiv (law), PsyArXiv (psychology), SocArXiv (social science), and SportRxiv (sport research) bubble to the top each day.

Papers are scored (in real-time) based on how verifiable they are (as determined by their Github repos) and how interesting they are (based on Twitter).

To see top papers, follow us on twitter @assertpub_ (arXiv), @assert_pub (bioRxiv), and @assertpub_dev (everything else).

To see beautiful figures extracted from papers, follow us on Instagram.

*Tracking 160,428 papers.*

Sort results based on if they are interesting or reproducible.

Interesting

Reproducible