From enhanced coinduction towards enhanced induction

There exist a rich and well-developed theory of enhancements of the coinduction proof method, widely used on behavioural relations such as bisimilarity. We study how to develop an analogous theory for inductive behaviour relations, i.e., relations defined from inductive observables. Similarly to the coinductive setting, our theory makes use of (semi)-progressions of the form R->F(R), where R is a relation on processes and F is a function on relations, meaning that there is an appropriate match on the transitions that the processes in R can perform in which the process derivatives are in F(R). For a given preorder, an enhancement corresponds to a sound function, i.e., one for which R->F(R) implies that R is contained in the preorder; and similarly for equivalences. We introduce weights on the observables of an inductive relation, and a weight-preserving condition on functions that guarantees soundness. We show that the class of functions contains non-trivial functions and enjoys closure properties with respect to desirable function constructors, so to be able to derive sophisticated sound functions (and hence sophisticated proof techniques) from simpler ones. We consider both strong semantics (in which all actions are treated equally) and weak semantics (in which one abstracts from internal transitions). We test our enhancements on a few non-trivial examples.

Limit theorems for Floyd's triangle: a new approach to not a new problem

Floyd's triangle is often presented to computer science students as an exercise or example to illustrate the concepts of text formatting and loop constructs. The paper proposes to look at an object from a different angle and to examine limit theorems for the numbers of generalized Floyd's triangles. Tasks of this type can be used as exercises in study programs of mathematics and informatics (couses of probability theory and combinatorics). It would help to master the appropriate proof techniques and mathematical apparatus. The article proposes a series of possible problems and their proof schemes.

Modeling and proving dynamic behaviors of a routing protocol: A tutorial

With the increasing adoption of Internet of Things technologies for controlling physical processes, their dependability becomes important. One of the fundamental functionalities on which such technologies rely for transferring information between devices is packet routing. However, while the performance of Internet of Things–oriented routing protocols has been widely studied experimentally, little work has been done on provable guarantees on their correctness in various scenarios. To stimulate this type of work, in this article, we give a tutorial on how such guarantees can be derived formally. Our focus is the dynamic behavior of distance-vector route maintenance in an evolving network. As a running example of a routing protocol, we employ routing protocol for low-power and lossy networks, and as the underlying formalism, a variant of linear temporal logic. By building a dedicated model of the protocol, we illustrate common problems, such as keeping complexity in control, modeling processing and communication, abstracting algorithms comprising the protocol, and dealing with open issues and external dependencies. Using the model to derive various safety and liveness guarantees for the protocol and conditions under which they hold, we demonstrate in turn a few proof techniques and the iterative nature of protocol verification, which facilitates obtaining results that are realistic and relevant in practice.

Foundations of regular coinduction

Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.

Compositional optimizations for CertiCoq

Compositional compiler verification is a difficult problem that focuses on separate compilation of program components with possibly different verified compilers. Logical relations are widely used in proving correctness of program transformations in higher-order languages; however, they do not scale to compositional verification of multi-pass compilers due to their lack of transitivity. The only known technique to apply to compositional verification of multi-pass compilers for higher-order languages is parametric inter-language simulations (PILS), which is however significantly more complicated than traditional proof techniques for compiler correctness. In this paper, we present a novel verification framework for lightweight compositional compiler correctness . We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through the same sequence of intermediate representations , logical relation proofs can be transitively composed in order to derive an end-to-end compositional specification for multi-pass compiler pipelines. Unlike traditional logical-relation frameworks, our framework supports divergence preservation—even when transformations reduce the number of program steps. We achieve this by parameterizing our logical relations with a pair of relational invariants . We apply this technique to verify a multi-pass, optimizing middle-end pipeline for CertiCoq, a compiler from Gallina (Coq’s specification language) to C. The pipeline optimizes and closure-converts an untyped functional intermediate language (ANF or CPS) to a subset of that language without nested functions, which can be easily code-generated to low-level languages. Notably, our pipeline performs more complex closure-allocation optimizations than the state of the art in verified compilation. Using our novel verification framework, we prove an end-to-end theorem for our pipeline that covers both termination and divergence and applies to whole-program and separate compilation, even when different modules are compiled with different optimizations. Our results are mechanized in the Coq proof assistant.

Improved Bounds for Centered Colorings

A vertex coloring $\phi$ of a graph $G$ is $p$-centered if for every connected subgraph $H$ of $G$ either $\phi$ uses more than $p$ colors on $H$ or there is a color that appears exactly once on $H$. Centered colorings form one of the families of parameters that allow to capture notions of sparsity of graphs: A class of graphs has bounded expansion if and only if there is a function $f$ such that for every $p\geq1$, every graph in the class admits a $p$-centered coloring using at most $f(p)$ colors. In this paper, we give upper bounds for the maximum number of colors needed in a $p$-centered coloring of graphs from several widely studied graph classes. We show that: (1) planar graphs admit $p$-centered colorings with $O(p^3\log p)$ colors where the previous bound was $O(p^{19})$; (2) bounded degree graphs admit $p$-centered colorings with $O(p)$ colors while it was conjectured that they may require exponential number of colors. All these upper bounds imply polynomial algorithms for computing the colorings. Prior to this work there were no non-trivial lower bounds known. We show that: (4) there are graphs of treewidth $t$ that require $\binom{p+t}{t}$ colors in any $p$-centered coloring. This bound matches the upper bound; (5) there are planar graphs that require $\Omega(p^2\log p)$ colors in any $p$-centered coloring. We also give asymptotically tight bounds for outerplanar graphs and planar graphs of treewidth $3$. We prove our results with various proof techniques. The upper bound for planar graphs involves an application of a recent structure theorem while the upper bound for bounded degree graphs comes from the entropy compression method. We lift the result for bounded degree graphs to graphs avoiding a fixed topological minor using the Grohe-Marx structure theorem.

Concrete domains in logics

In this short survey, we present logical formalisms in which reasoning about concrete domains is embedded in formulae at the atomic level. These include temporal logics with concrete domains, description logics with concrete domains as well as variant formalisms. We discuss several proof techniques to solve logical decision problems for such formalisms, including those based on constrained automata or on translation into decidable second-order logics. We also present recent results mainly related to decidability and complexity as well as a selection of open problems.

Discrete Mathematics into K-11 and K-12 Grade Education

Discrete mathematics is one of the significant part of K-11 and K-12 grade college classrooms. In this contribution, we discuss the usefulness of basic elementary, some of the intermediate discrete mathematics for K-11 and K-12 grade colleges. Then we formulate the targets and objectives of this education study. We introduced the discrete mathematics topics such as set theory and their representation, relations, functions, mathematical induction and proof techniques, counting and its underlying principle, probability and its theory and mathematical reasoning. Core of this contribution is proof techniques, counting and mathematical reasoning. Since all these three concepts of discrete mathematics is strongly connected and creates greater impact on students. Moreover, it is potentially useful in their life also out of the college study. We explain the importance, applications in computer science and the comments regarding introduction of such topics in discrete mathematics. Last part of this article provides the theoretical knowledge and practical usability will strengthen the made them understand easily.

Review of The Theory of Quantum Information John Watrous

This is an extremely clear, carefully written book that covers the most important results in the sprawling field of quantum information. It is perfect for a reference, self-study, or a graduate course in quantum information. It makes no attempt to be broad or encyclopedic, but instead goes deep into the core topics. The definitions and theorems are all precisely worded, and (starting in Chapter 2) all results have complete proofs, making the book largely self-contained. The book focuses heavily on the mathematical results and nuts-and-bolts techniques underpinning current research, and as such gives the reader a thorough and flexible toolkit for proving new results. If you are just looking for a broad but cursory survey of the field, then this is probably not the book for you. If, however, you want a working knowledge of the core results and proof techniques of quantum information with an eye toward doing cutting-edge research in the field, then this book will be an indispensable addition to your library. The mathematical theory of quantum information studies the ultimate abilities and limits of transmitting and processing information using the laws of quantum mechanics. It owes much of its motivation to classical information theory, which was largely developed by Claude Shannon in the mid 20th century, and to quantum mechanics itself (of course). It addresses basic questions like: how much information can be transmitted through quantum channels, noisy or otherwise, and how entanglement helps. The theory informs, and is informed by, its sister disciplines of quantum computation and quantum communication (which overlap with physics and computer science), although in some sense it is more fundamental. Though he occasionally mentions applications to these other areas, Watrous seats his book squarely in the realm of pure mathematics.