Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userProof Pearl: Magic Wand as Frame
52
0
0.0
(
0
)
Added by
Qinxiang Cao
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Separation logic adds two connectives to assertion languages: separating conjunction * (star) and its adjoint, separating implication -* (magic wand). Comparatively, separating implication is less widely used. This paper demonstrates that by using magic wand to express frames that relate mutable local portions of data structures to global portions, we can exploit its power while proofs are still easily understandable. Many useful separation logic theorems about partial data structures can now be proved by simple automated tactics, which were usually proved by induction. This magic-wand-as-frame technique is especially useful when formalizing the proofs by a high order logic. We verify binary search tree insert in Coq as an example to demonstrate this proof technique.
rate research
Read More
The theory of program modules is of interest to language designers not only for its practical importance to programming, but also because it lies at the nexus of three fundamental concerns in language design: the phase distinction, computational effects, and type abstraction. We contribute a fresh synthetic take on program modules that treats modules as the fundamental constructs, in which the usual suspects of prior module calculi (kinds, constructors, dynamic programs) are rendered as derived notions in terms of a modal type-theoretic account of the phase distinction. We simplify the account of type abstraction (embodied in the generativity of module functors) through a lax modality that encapsulates computational effects. Our main result is a (significant) proof-relevant and phase-sensitive generalization of the Reynolds abstraction theorem for a calculus of program modules, based on a new kind of logical relation called a parametricity structure. Parametricity structures generalize the proof-irrelevant relations of classical parametricity to proof-relevant families, where there may be non-trivial evidence witnessing the relatedness of two programs -- simplifying the metatheory of strong sums over the collection of types, for although there can be no relation classifying relations, one easily accommodates a family classifying small families. Using the insight that logical relations/parametricity is itself a form of phase distinction between the syntactic and the semantic, we contribute a new synthetic approach to phase separated parametricity based on the slogan logical relations as types, iterating our modal account of the phase distinction. Then, to construct a simulation between two implementations of an abstract type, one simply programs a third implementation whose type component carries the representation invariant.
Tensor kernels in machine learning (ML) often correspond to pure mathematical expressions, making term rewriting an attractive strategy for optimization and mapping to specialized hardware accelerators. However, existing ML intermediate representations (IRs) tend to either be textit{pure but high-level}, making low-level rewrites to hardware targets inexpressible, or textit{low-level but impure}, hampering the use of term rewriting altogether. This paper introduces Glenside, a pure IR whose core abstraction -- the textit{access pattern} -- enables low-level, layout-aware, hardware-centric program rewrites. We demonstrate how term rewriting in Glenside can be used to map program fragments to hardware accelerator invocations and automatically discover classic data layout transformations like texttt{im2col}. Glenside establishes a new foundation for exploring further term rewriting techniques in optimizing low-level tensor programs.
Context. Galaxies in the Universe form chains (filaments) that connect groups and clusters of galaxies. The filamentary network includes nearly half of the galaxies and is visually the most striking feature in cosmological maps. Aims. We study the distribution of galaxies along the filamentary network, trying to find specific patterns and regularities. Methods. Galaxy filaments are defined by the Bisous model, a marked point process with interactions. We use the two-point correlation function and the Rayleigh Z-squared statistic to study how galaxies and galaxy groups are distributed along the filaments. Results. We show that galaxies and groups are not uniformly distributed along filaments, but tend to form a regular pattern. The characteristic length of the pattern is around 7 Mpc/h. A slightly smaller characteristic length 4 Mpc/h can also be found, using the Z-squared statistic. Conclusions. We find that galaxy filaments in the Universe are like pearl necklaces, where the pearls are galaxy groups distributed more or less regularly along the filaments. We propose that this well defined characteristic scale could be used to test various cosmological models and to probe environmental effects on the formation and evolution of galaxies.
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe program is used for critical systems. Therefore, formal methods for these kinds of systems are greatly required. In this paper, we use a formal language that performs deductive verification on an Ethereum Blockchain application based on smart contracts, which are self-executing digital contracts. Blockchain systems manipulate cryptocurrency and transaction information. Therefore , if a bug occurs in the blockchain, serious consequences such as a loss of money can happen. Thus, the aim of this paper is to propose a language dedicated to deductive verification, called Why3, as a new language for writing formal and verified smart contracts, thereby avoiding attacks exploiting such contract execution vulnerabilities. We first write a Why3 smart contracts program; next we formulate specifications to be proved as absence of RunTime Error properties and functional properties, then we verify the behavior of the program using the Why3 system. Finally we compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreover, we give a set of generic mathematical statements that allows verifying functional properties suited to any type of smart contracts holding cryptocurrency, showing that Why3 can be a suitable language to write smart contracts. To illustrate our approach, we describe its application to a realistic industrial use case.
An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates almost surely. Proving that can be hard, and this paper presents a new method for doing so; it is expressed in a program logic, and so applies directly to source code. The programs may contain both probabilistic- and demonic choice, and the probabilistic choices may depend on the current state. As do other researchers, we use variant functions (a.k.a. super-martingales) that are real-valued and probabilistically might decrease on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
