### Top 8 Arxiv Papers Today in Logic In Computer Science

##### #1. Formal verification of trading in financial markets
###### Suneel Sarswat, Abhishek Kr Singh
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.
###### Tweets
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.
###### Other stats
Sample Sizes : None.
Authors: 2
Total Words: 0
Unqiue Words: 0

##### #2. Typal Heterogeneous Equality Types
###### Andrew M. Pitts
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.
###### Tweets
arxiv_cslo: Typal Heterogeneous Equality Types https://t.co/lxDsz8CEnT
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 4550
Unqiue Words: 1166

##### #3. Defining Functions on Equivalence Classes
###### Lawrence C. Paulson
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.
###### Tweets
arxiv_cslo: Defining Functions on Equivalence Classes https://t.co/Xo0OT1R4eP
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 1
Total Words: 7515
Unqiue Words: 2138

##### #4. Mutation Testing with Hyperproperties
###### Andreas Fellner, Mitra Tabaei Befrouei, Georg Weissenbacher
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.
###### Tweets
arxiv_cslo: Mutation Testing with Hyperproperties https://t.co/EhIIdw9bZV
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

##### #5. Shallow Embedding of Type Theory is Morally Correct
###### Ambrus Kaposi, András Kovács, Nicolai Kraus
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.
###### Tweets
arxiv_cslo: Shallow Embedding of Type Theory is Morally Correct https://t.co/uYz38A85v3
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

##### #6. Priorities in tock-CSP
###### Pedro Ribeiro, James Baxter, Ana Cavalcanti
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.
###### Tweets
arxiv_cslo: Priorities in tock-CSP https://t.co/HqOt7hiPEJ
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 3
Total Words: 7078
Unqiue Words: 1517

##### #7. Runtime Verification For Timed Event Streams With Partial Information
###### Martin Leucker, César Sánchez, Torben Scheffel, Malte Schmitz, Daniel Thoma
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.
###### Tweets
arxiv_cslo: Runtime Verification For Timed Event Streams With Partial Information https://t.co/IH4BH9F93V
None.
None.
###### Other stats
Sample Sizes : None.
Authors: 5
Total Words: 0
Unqiue Words: 0

##### #8. Delta -- new logic programming language and Delta-methodology for p-computable programs on Turing Complete Languages
###### Andrey Nechesov
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.
###### Tweets
arxiv_cslo: Delta -- new logic programming language and Delta-methodology for p-computable programs on Turing Complete Languages https://t.co/SOsuzWhyQ9
None.
None.
###### Other stats
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.

###### Search
Sort results based on if they are interesting or reproducible.
Interesting
Reproducible
Online
###### Stats
Tracking 160,428 papers.