Top 8 Arxiv Papers Today in Logic In Computer Science


2.048 Mikeys
#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
Figures
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
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 2
Total Words: 0
Unqiue Words: 0

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Typal Heterogeneous Equality Types https://t.co/lxDsz8CEnT
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 4550
Unqiue Words: 1166

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Defining Functions on Equivalence Classes https://t.co/Xo0OT1R4eP
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 7515
Unqiue Words: 2138

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Mutation Testing with Hyperproperties https://t.co/EhIIdw9bZV
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Shallow Embedding of Type Theory is Morally Correct https://t.co/uYz38A85v3
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 0
Unqiue Words: 0

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Priorities in tock-CSP https://t.co/HqOt7hiPEJ
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 3
Total Words: 7078
Unqiue Words: 1517

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Runtime Verification For Timed Event Streams With Partial Information https://t.co/IH4BH9F93V
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 5
Total Words: 0
Unqiue Words: 0

1.999 Mikeys
#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
Figures
None.
Tweets
arxiv_cslo: Delta -- new logic programming language and Delta-methodology for p-computable programs on Turing Complete Languages https://t.co/SOsuzWhyQ9
Github
None.
Youtube
None.
Other stats
Sample Sizes : None.
Authors: 1
Total Words: 0
Unqiue Words: 0

About

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
Categories
All
Astrophysics
Cosmology and Nongalactic Astrophysics
Earth and Planetary Astrophysics
Astrophysics of Galaxies
High Energy Astrophysical Phenomena
Instrumentation and Methods for Astrophysics
Solar and Stellar Astrophysics
Condensed Matter
Disordered Systems and Neural Networks
Mesoscale and Nanoscale Physics
Materials Science
Other Condensed Matter
Quantum Gases
Soft Condensed Matter
Statistical Mechanics
Strongly Correlated Electrons
Superconductivity
Computer Science
Artificial Intelligence
Hardware Architecture
Computational Complexity
Computational Engineering, Finance, and Science
Computational Geometry
Computation and Language
Cryptography and Security
Computer Vision and Pattern Recognition
Computers and Society
Databases
Distributed, Parallel, and Cluster Computing
Digital Libraries
Discrete Mathematics
Data Structures and Algorithms
Emerging Technologies
Formal Languages and Automata Theory
General Literature
Graphics
Computer Science and Game Theory
Human-Computer Interaction
Information Retrieval
Information Theory
Machine Learning
Logic in Computer Science
Multiagent Systems
Multimedia
Mathematical Software
Numerical Analysis
Neural and Evolutionary Computing
Networking and Internet Architecture
Other Computer Science
Operating Systems
Performance
Programming Languages
Robotics
Symbolic Computation
Sound
Software Engineering
Social and Information Networks
Systems and Control
Economics
Econometrics
General Economics
Theoretical Economics
Electrical Engineering and Systems Science
Audio and Speech Processing
Image and Video Processing
Signal Processing
General Relativity and Quantum Cosmology
General Relativity and Quantum Cosmology
High Energy Physics - Experiment
High Energy Physics - Experiment
High Energy Physics - Lattice
High Energy Physics - Lattice
High Energy Physics - Phenomenology
High Energy Physics - Phenomenology
High Energy Physics - Theory
High Energy Physics - Theory
Mathematics
Commutative Algebra
Algebraic Geometry
Analysis of PDEs
Algebraic Topology
Classical Analysis and ODEs
Combinatorics
Category Theory
Complex Variables
Differential Geometry
Dynamical Systems
Functional Analysis
General Mathematics
General Topology
Group Theory
Geometric Topology
History and Overview
Information Theory
K-Theory and Homology
Logic
Metric Geometry
Mathematical Physics
Numerical Analysis
Number Theory
Operator Algebras
Optimization and Control
Probability
Quantum Algebra
Rings and Algebras
Representation Theory
Symplectic Geometry
Spectral Theory
Statistics Theory
Mathematical Physics
Mathematical Physics
Nonlinear Sciences
Adaptation and Self-Organizing Systems
Chaotic Dynamics
Cellular Automata and Lattice Gases
Pattern Formation and Solitons
Exactly Solvable and Integrable Systems
Nuclear Experiment
Nuclear Experiment
Nuclear Theory
Nuclear Theory
Physics
Accelerator Physics
Atmospheric and Oceanic Physics
Applied Physics
Atomic and Molecular Clusters
Atomic Physics
Biological Physics
Chemical Physics
Classical Physics
Computational Physics
Data Analysis, Statistics and Probability
Physics Education
Fluid Dynamics
General Physics
Geophysics
History and Philosophy of Physics
Instrumentation and Detectors
Medical Physics
Optics
Plasma Physics
Popular Physics
Physics and Society
Space Physics
Quantitative Biology
Biomolecules
Cell Behavior
Genomics
Molecular Networks
Neurons and Cognition
Other Quantitative Biology
Populations and Evolution
Quantitative Methods
Subcellular Processes
Tissues and Organs
Quantitative Finance
Computational Finance
Economics
General Finance
Mathematical Finance
Portfolio Management
Pricing of Securities
Risk Management
Statistical Finance
Trading and Market Microstructure
Quantum Physics
Quantum Physics
Statistics
Applications
Computation
Methodology
Machine Learning
Other Statistics
Statistics Theory
Feedback
Online
Stats
Tracking 160,428 papers.