Search

A mosquito born viral disease (Dengue) becoming endemic around the globe which including cause of severe illness and death in various Asian and Latin American countries. It needs proper management by researchers and medicine professionals. The current research work is a step towards the prevention/reduction of such deadly disease in the society. More precisely, this work addressing various mathematical proofs interconnected to the existence and stability along with numerical findings by using mathematical modeling techniques. Further, the existence results have been established for the proposed model under the Atangana-Baleanu derivative in Caputo sense (ABC) with fractional order. In continuation, we find the deterministic stability for the proposed model. Lastly, the new version of numerical approximation’s framework for the approximation of ABC fractional derivative is used to carried out the numerical simulation for the obtained results.

We present a new method to extract from a classical proof of ∀x(I[x]→∃y(O[y]∧S[x,y])) a program computing y from x. This method applies when O is a data type and S is a decidable predicate. Algorithms extracted this way are often far better than a stupid enumeration of all the possible outputs and this is verified on a nontrivial example: a proof of Dickson's lemma.

The probabilistic guarded-command language pGCL [Carroll Morgan, Annabelle McIver. pGCL: formal reasoning for random algorithms. South African Computer Journal (1999)] contains both demonic and probabilistic nondeterminism, which makes it suitable for reasoning about distributed random algorithms [Carroll Morgan. Proof rules for probabilistic loops. In Proceedings of the BCS-FACS 7th Refinement Workshop. He Jifeng, John Cooke and Peter Wallis (eds). Springer Verlag Workshops in Computing, 1996]. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-) valued functions.We present a mechanization of the quantitative logic for pGCL [Carroll Morgan, Annabelle McIver, and Karen Seidel, Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3): 325–353, May 1996] using the HOL theorem prover [M.J.C. Gordon and T.F. Melham. Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, 1993], including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL [E.W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976].The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm [Eyal Kushilevitz and Michael O. Rabin. Randomized mutual exclusion algorithms revisited. In Maurice Herlihy, editor, Proceedings of the 11th Annual Symposium on Principles of Distributed Computing, pages 275–283, Vancouver, BC, Canada, August 1992. ACM Press].

We present an extension of Heyting arithmetic in finite types called Uniform Heyting Arithmetic ( HA u ) that allows for the extraction of optimized programs from constructive and classical proofs. The system HA u has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program.

There are two ways to define a semantics for process algebras: either directly by means of an equivalence relation or by means of a preorder whose kernel is the desired equivalence. We are interested in the relationship between these two presentations. Using our characterisation of the behaviour preorders by means of simulations up-to we were able to generate the canonical preorders corresponding to each behaviour equivalence. The axiomatizations of these preorders can be obtained by adding to the axioms of the equivalence that of the appropriate simulation. Aceto, Fokkink and Ingólfsdóttir have presented an algorithm that goes in the opposite direction, constructing an axiomatization of the induced equivalence from that of a given preorder. Following a different path we were able to get a correct proof and an enhanced algorithm. In this paper we present an shorter and simpler proof of this result, based on our coinductive characterisations of the behaviour preorders, and in particular in the existence of the canonical preorders. More important, we also present further generalisations of the result, since our coinductive characterisations are not only valid for the semantics coarser than the ready simulation.By means of these new proofs and results we hope to contribute to a better knowledge of the semantics of processes and to better understand the tight relations between preorders and equivalences that define them.

Given any subset A of ω 1 there is a proper partial order which forces that the predicate x ∈ A and the predicate x ∈ ω 1 ∖ A can be expressed by ZFC -provably incompatible Σ 3 formulas over the structure 〈 H ω 2 , ∈ , N S ω 1 〉 . Also, if there is an inaccessible cardinal, then there is a proper partial order which forces the existence of a well-order of H ω 2 definable over 〈 H ω 2 , ∈ , N S ω 1 〉 by a provably antisymmetric Σ 3 formula with two free variables. The proofs of these results involve a technique for manipulating the guessing properties of club-sequences defined on stationary subsets of ω 1 at will in such a way that the Σ 3 theory of 〈 H ω 2 , ∈ , N S ω 1 〉 with countable ordinals as parameters is forced to code a prescribed subset of ω 1 . On the other hand, using theorems due to Woodin it can be shown that, in the presence of sufficiently strong large cardinals, the above results are close to optimal from the point of view of the Levy hierarchy.

A family F of k-graphs is called non-principal if its Turán density is strictly smaller than that of each individual member. For each k⩾3 we find two (explicit) k-graphs F and G such that {F,G} is non-principal. Our proofs use stability results for hypergraphs. This completely settles the question posed by Mubayi and Rödl [On the Turán number of triple systems, J. Combin. Theory A, 100 (2002) 135–152].Also, we observe that the demonstrated non-principality phenomenon holds also with respect to the Ramsey–Turán density as well.

Scale elasticity (SE) and returns to scale (RTS) are important topics in performance analysis, which help managers to make decisions about the expansion or contraction of the operation of decision making units under assessment. In this paper, some new results about these topics in the presence of alternative solutions, regarding the concept of multifunction, are provided.At first, some properties of some multifunctions (functions), defined with respect to the optimal solutions of DEA models, are established which help us in what follows. In turn, the relationships between the considered multifunctions and the concept of RTS and SE are studied. Finally an approach for the estimation of the RTS classification of units is obtained, which leads to an important corollary as an interesting result which introduces a connection between two concepts, RTS and SE. This is important from an applied point of view. Also, from a technical point of view, the proofs of theorems which give this corollary use a main lemma of convex analysis literature and give a constructive proof about RTS.

This paper continues the investigation of tiling problems via formal languages, which was begun in papers by Merlini, Sprugnoli, and Verri. Those authors showed that certain tiling problems could be encoded by regular languages, which lead automatically to generating functions and other combinatorial information on tilings. We introduce a method of simplifying the DFA’s recognizing these language, which leads to bijective proofs of certain tiling identities. We apply these ideas to some other tiling problems, including three-dimensional tilings and tilings with triangles and rhombi. We also study graph-theoretic variations of these tiling problems.

We present proofs of lower bounds on the node search number of some grid-like graphs including two-dimensional grids, cylinders, tori and a variation we call “orb-webs”. Node search number is equivalent to pathwidth and vertex separation, which are all important graph parameters. Since matching upper bounds are not difficult to obtain, this implies that the pathwidth of these graphs is easily computed, because the bounds are simple functions of the graph dimensions. We also show matching upper and lower bounds on the node search number of equidimensional tori which are one less than the obvious upper bound.

We describe a tool that combines a general purpose theorem prover and an ofi-theshelf interface for dynamic geometry drawing to enhance man-machine interaction involving geometrical proofs. With our tool, we can edit the statements of geometrical theorems, construct and verify their proofs with the theorem prover, and visualize the statements using the drawing tool. The key component is an algorithm that computes the data needed to draw a construction from the formal statement of the theorem. The paper includes some examples of output from our combined tool, called GeoView.

We present a new transformation of λ-terms into continuation-passing style (CPS). This transformation operates in one pass and is both compositional and first-order. Previous CPS transformations only enjoyed two out of the three properties of being first-order, one-pass, and compositional, but the new transformation enjoys all three properties. It is proved correct directly by structural induction over source terms instead of indirectly with a colon translation, as in Plotkin's original proof. Similarly, it makes it possible to reason about CPS-transformed terms by structural induction over source terms, directly.The new CPS transformation connects separately published approaches to the CPS transformation. It has already been used to state a new and simpler correctness proof of a direct-style transformation, and to develop a new and simpler CPS transformation of control-flow information.

A Sudoku grid is a 9x9 Latin square further constrained to have nine non-overlapping 3x3 mini-grids each of which contains the values 1-9. In @D-Quasi-Magic Sudoku a further constraint is imposed such that every row, column and diagonal in each mini-grid sums to an integer in the interval [[email protected],[email protected]]. The problem of proving certain (computationally known) results for @D=2 concerning mini-grids and bands (rows of mini-grids) was posed at the British Combinatorial Conference in 2007. These proofs are presented and extensions of these provide a full combinatorial enumeration for the total number of completed 2-Quasi-Magic Sudoku grids. It is also shown that there are 40 isomorphism classes of completed 2-Quasi-Magic Sudoku grids.

This paper introduces a notion of certified computation whereby an algorithm not only produces a result r for a given input x, but also proves that r is a correct result for x. This can greatly enhance the credibility of the result: if we trust the axioms and inference rules that are used in the proof, then we can be assured that r is correct. Typically, the reasoning used in a certified computation is much simpler than the computation itself. We present and analyze two examples of certifying algorithms.We have developed denotational proof languages (DPLs) as a uniform platform for certified computation. DPLs integrate computation and deduction seamlessly, offer strong soundness guarantees, and provide versatile mechanisms for constructing proofs and proof-search methods. We have used DPLs to implement numerous well-known algorithms as certifiers, ranging from sorting algorithms to compiler optimizations, the Hindley-Milner W algorithm, Prolog engines, and more.

We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider's generalized clock synchronization protocol [Schneider, F. B., Understanding protocols for Byzantine clock synchronization, Technical Report TR 87–859, Cornell University (1987). URL citeseer.ist.psu.edu/schneider87understanding.html] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [Lamport, L. and P. M. Melliar-Smith, Synchronizing clocks in the presence of faults, J. ACM 32 (1985), pp. 52–78] and the Fault-tolerant Midpoint algorithm of Lundelius-Lynch [Lundelius, J. and N. Lynch, A new fault-tolerant algorithm for clock synchronization, in: Proceedings of PODC '84 (1984), pp. 75–88], satisfy Schneider's general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify the parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetic like ICS and CVC Lite.

GeoThms is a web-based framework for exploring geometrical knowledge that integrates Dynamic Geometry Software (DGS), Automatic Theorem Provers (ATP), and a repository of geometrical constructions, figures and proofs. The GeoThms users can easily use/browse through existing geometrical content and build new contents. In this paper we describe GeoThms functionalities, focusing on the interface solutions required for a system aimed at supporting studying and teaching geometry via Internet. GeoThms is a publicly accessible system with a growing body of geometrical constructions and formally proven geometrical theorems. We believe that, with the help of all its users it will become an important Internet resource for geometry.

This article presents formalized intuitionistic proofs for the polyhedra genus theorem, the Euler formula and a sufficient condition of planarity. They are based on a hypermap model for polyhedra and on formal specifications in the Calculus of Inductive Constructions. First, a type of free maps is inductively defined from three atomic constructors. Next, a hierarchy of types defined by invariants, with operations constrained by preconditions, is built on the free maps: hypermaps, orientated combinatorial maps and a central notion of quasi-hypermaps. Besides, the proofs of their properties are established until the genus theorem and the Euler formula, mainly using a simple induction principle based on the free map term algebra. Finally, a constructive sufficient condition for polyhedra to be planar is set and proved. The whole process is assisted by the interactive Coq proof system.

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof, but standard techniques for the construction of appropriate induction rules are restricted to recycling the recursive structure of the specifications. What is needed is induction rule construction techniques that can introduce novel recursive structures. We show that a combination of rippling and the use of meta-variables as a least-commitment device can provide such novelty.

International audience; We present the design of the Boost interval arithmetic library, a C++ library designed to efficiently handle mathematical intervals in a generic way. Interval computations are an essential tool for reliable computing. Increasingly a number of mathematical proofs have relied on global optimization problems solved using branch-and-bound algorithms with interval computations; it is therefore extremely important to have a mathematically correct implementation of interval arithmetic. Various implementations exist with diverse semantics. Our design is unique in that it uses policies to specify three independent variable behaviors: rounding, checking, comparisons. As a result, with the proper policies, our interval library is able to emulate almost any of the specialized libraries available for interval arithmetic, without any loss of performance nor sacrificing the ease of use. This library is openly available at www.boost.org.

For the problem (here u=u(x)) Δu−up+αuq+βur=0,x∈Rn,lim|x|→∞u(x)=0, with constants 1≤p0, uniqueness of radial solution (calledground state solution) is not known. We present a procedure, which opens the way to produce computer assisted proofs of uniqueness for specific p, q, r, and n.

The reversed compound agent theorem (RCAT) is a compositional result that uses Markovian process algebra (MPA) to derive the reversed process of certain interactions between two continuous time Markov chains at equilibrium. From this reversed process, together with the given, forward process, the joint state probabilities can be expressed as a product-form, although no general algorithm has previously been given. This paper first generalises RCAT to multiple (more than two) cooperating agents, which removes the need for multiple applications and inductive proofs in cooperations of an arbitrary number of processes. A new result shows a simple stochastic equivalence between cooperating, synchronised processes and corresponding parallel, asynchronous processes. This greatly simplifies the proof of the new, multi-agent theorem, which includes a statement of the desired product-form solution itself as a product of given state probabilities in the parallel components. The reversed process and product-form thus derived rely on a solution to certain rate equations and it is shown, for the first time, that a unique solution exists under mild conditions—certainly for queueing networks and G-networks.

Affine terms are lambda terms in which no variable occurs twice, and linear terms are affine terms in which each bound variable occurs exactly once. The principal type of a term is the most general type which is assignable to the term. Hirokawa gave characterisations of the principal types of linear terms and of beta-normal affine terms. Shouji gave a characterisation of the principal types of beta-eta-normal linear terms. The proofs of these three theorems are parallel, but independent to each other. This paper points out that by using Berardi's pruning, the theorem on beta-normal affine terms is obtained from the theorem on linear terms. This is the first result. And also this paper shows a characterisation of principal types of beta-eta-normal affine terms. Its proof is obtained from the theorem on beta-eta-normal linear terms by Berardi's pruning. This is the second result. Besides, this paper gives other proofs of the the theorems on eta-normal terms. This is the third result.

This paper investigates some delicate tradeoffs between the generality of an algorithmic learning device and the quality of the programs it learns successfully. There are results to the effect that, thanks to small increases in generality of a learning device, the computational complexity of some successfully learned programs is provably unalterably suboptimal. There are also results in which the complexity of successfully learned programs is asymptotically optimal and the learning device is general, but, still thanks to the generality, some of those optimal, learned programs are provably unalterably information deficient—in some cases, deficient as to safe, algorithmic extractability/provability of the fact that they are even approximately optimal. For these results, the safe, algorithmic methods of information extraction will be by proofs in arbitrary, true, computably axiomatizable extensions of Peano Arithmetic.

We show that the KKM principle implies two new general fixed point theorems for the Kakutani maps or the Browder maps. Consequently, we give unified transparent proofs of many of well-known results.

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.

An overview is given of ACP with conditional composition (i.e., if-then-else) over Belnap's four-valued logic. The interesting thing is that much of ACP can be analyzed using this logic. For example, both the choice operation + and δ (deadlock) can be seen as instances of conditional composition, and the axiom x + δ = x follows from this perspective. Furthermore, parallel composition can be generalized to conditional parallel composition, which has sequential composition as an instance, next to common parallel composition, pure interleaving and synchronous ACP. This article is an extended abstract of [A. Ponse, M.B. van der Zwaag. A generalization of ACP using Belnap's logic. Submitted to Journal of Logic and Algebraic Programming]. The full article contains all proofs and some examples on parallel scheduling in GACP.

This paper presents the architecture and functionality of a logic prover designed for question answering. The approach transforms questions and answer passages into logic representations based on syntactic, semantic and contextual information. World knowledge supplements the linguistic, ontological, and temporal axioms supplied to the prover which renders a deep understanding of the relationship between the question and answer text. The trace of the proofs provides a basis for generating human comprehensible answer justifications. The results show that the prover boosts the performance of the Question Answering system on TREC 2004 questions by 12%.

In this paper, we give some metrization theorems and characterize some generalized metric spaces in terms of (weak base) g -functions. And we give quick proofs of two theorems in [Topology Appl. 91 (1999) 71].

This paper describes an experimental system called ProveEasy for helping people learn to write Natural Deduction proofs in a goal directed style. The proof is an editable text, produced by typing or by pointing and clicking. The intended users are people who write programs, and the representation of proofs is analogous to the usual representation of programs. Emphasis is placed on distinguishing what is given from what is to be shown at each stage. The presentation shows the way the proof was discovered. The work is inspired by type theory proof assistants, but it attempts to hide the difficulties of such powerful systems.

The paper is dealing with the problem of finding the densest packings of equal circles in the unit square. Recently, a global optimization method based exclusively on interval arithmetic calculations has been designed for this problem. With this method it became possible to solve the previously open problems of packing 28, 29, and 30 circles in the numerical sense: tight guaranteed enclosures were given for all the optimal solutions and for the optimum value. The present paper completes the optimality proofs for these cases by determining all the optimal solutions in the geometric sense. Namely, it is proved that the currently best-known packing structures result in optimal packings, and moreover, apart from symmetric configurations and the movement of well-identified free circles, these are the only optimal packings. The required statements are verified with mathematical rigor using interval arithmetic tools.

This paper analyses two fundamental notes by Stone, giving two ways of representing a compact space in term of some algebra of functions over this space, in the framework of point-free topology. As applications, we give an alternative approach to the spectral theorem, and we present constructive proofs of results of Krivine and of the Kadison-Dubois theorem.

We describe a new way to model deletion operations on formal languages, called deletion along trajectories. We examine its closure properties, which differ from those of shuffle on trajectories, previously introduced by Mateescu et al. In particular, we define classes of non-regular sets of trajectories such that the associated deletion operation preserves regularity. Our results give uniform proofs of closure properties of the regular languages for several deletion operations.We also show that deletion along trajectories serves as an inverse to shuffle on trajectories. This leads to results on the decidability of certain language equations, including those of the form LTX=R, where L,R are regular languages and X is unknown.

Let S be a numerical semigroup and let p be a positive integer. Then the quotient S p = { x ∈ N ∣ p x ∈ S } is also a numerical semigroup. When p = 2 we say that S 2 is half of the numerical semigroup S . Dually, we say that S is a double of the numerical semigroup S 2 . We characterize the set of all doubles of a numerical semigroup. We also give some alternative proofs and improvements for some results that we find in previous papers.

As part of a project on automatic generation of proofs involving both logic and computation, we have automatically generated a proof of the irrationality of e. The proof involves inequalities, bounds on infinite series, type distinctions (between real numbers and natural numbers), a subproof by mathematical induction, and significant mathematical steps, including correct simplification of expressions involving factorials and summing an infinite geometrical series. Metavariables are instantiated by inference rules embodying mathematical knowledge, rather than only by unification. The proof is generated completely automatically, without any interactive component.

In [P. Hancock, A. Setzer, Interactive programs in dependent type theory, in: P. Clote, H. Schwichtenberg (Eds.), Proc. 14th Annu. Conf. of EACSL, CSL’00, Fischbau, Germany, 21–26 August 2000, Vol. 1862, Springer, Berlin, 2000, pp. 317–331, URL 〈citeseer.ist.psu.edu/article/hancock00interactive.html〉; P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in: L. Crosilla, P. Schuster (Eds.), From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, Oxford Logic Guides, Clarendon Press, 2005, URL 〈www.cs.swan.ac.uk/∼csetzer/〉] Hancock and Setzer introduced rules to extend Martin-Löf's type theory in order to represent interactive programming. The rules essentially reflect the existence of weakly final coalgebras for a general form of polynomial functor. The standard rules of dependent type theory allow the definition of inductive types, which correspond to initial algebras. Coalgebraic types are not represented in a direct way. In this article we show the existence of final coalgebras in intensional type theory for these kind of functors, where we require uniqueness of identity proofs (UIP) for the set of states S and the set of commands C which determine the functor. We obtain the result by identifying programs which have essentially the same behaviour, viz. are bisimular. This proves the rules of Setzer and Hancock admissible in ordinary type theory, if we replace definitional equality by bisimulation. All proofs [M. Michelbrink, Verifications of final coalgebra theorem in: Interfaces as Functors, Programs as Coalgebras—A Final Coalgebra Theorem in Intensional Type Theory, 2005, URL 〈www.cs.swan.ac.uk/∼csmichel/〉] are verified in the theorem prover agda [C. Coquand, Agda, Internet, URL 〈www.cs.chalmers.se/∼catarina/agda/〉; K. Peterson, A programming system for type theory, Technical Report, S-412 96, Chalmers University of Technology, Göteborg, 1982], which is based on intensional Martin-Löf type theory.

Protocol composition logic, PCL, is a formal approach for proving security properties of a class of network protocols. PCL involves reasoning directly about properties achieved by protocols steps, in a setting that does not require explicit reasoning about attacker actions. The method relies on protocol invariants to combine properties of different roles of a protocol. While some protocol invariants can be complex to identify and prove, many useful PCL invariants are relatively straightforward consequences of the programs (roles) executed by the agents involved in the protocol. We present a logic program based approach for automating proofs of invariants that appears effective for invariants that are required for several standardized, widely deployed protocols. We use the well-known Transport Layer Security Protocol (TLS/SSL) to illustrate the approach.

In this paper we investigate weighted cross-intersecting families: if α,β>0 are given constants, we want to find the maximum of α|A|+β|B| for A,B uniform cross-intersecting families. We determine the maximum sum, even if we have restrictions of the size of A.As corollaries, we will obtain some new bounds on the shadows and the shades of uniform families. We give direct proofs for these bounds, as well, and show that the theorems for cross-intersecting families also follow from these results.Finally, we will generalize the LYM inequality not only for cross-intersecting families, but also for arbitrary Sperner families.

The Cartan–Dieudonne–Scherk Theorem states that for fields of characteristic other than 2, every orthogonality can be written as the product of a certain minimal number of reflections across hyperplanes. The earliest proofs are not constructive, and constructive proofs either do not achieve minimal results or have been restricted to special cases. This paper presents a constructive proof in the real or complex field of the decomposition of a generalized orthogonal matrix into the product of the minimal number of generalized Householder matrices.

Permutative logic is a non-commutative conservative extension of linear logic suggested by some investigations on the topology of linear proofs. In order to syntactically reflect the fundamental topological structure of orientable surfaces with boundary, permutative sequents turn out to be shaped like q-permutations. Relaxation is the relation induced on q-permutations by the two structural rules divide and merge; a decision procedure for relaxation has been already provided by stressing some standard achievements in theory of permutations. In these pages, we provide a parallel procedure in which the problem at issue is approached from the point of view afforded by geometry of 2-manifolds and solved by making specific surfaces interact.

This paper presents a formal framework for compositional reasoning about secure systems. A key insight is to view a trusted system in terms of the interfaces that the various components expose: larger trusted components are built by combining interface calls in known ways; the adversary is confined to the interfaces it has access to, but may combine interface calls without restriction. Compositional reasoning for such systems is based on an extension of rely-guarantee reasoning for system correctness [Misra, J. and K.M. Chandy, Proofs of networks of processes, IEEE Transactions on Software Engineering 7 (1981), pp. 417–426; Jones, C.B., Tentative steps toward a development method for interfering programs, ACM Transactions on Programming Languages and Systems (TOPLAS) 5 (1983), pp. 596–619] to a setting that involves an adversary whose exact program is not known. At a technical level, the paper presents an expressive concurrent programming language with recursive functions for modeling interfaces and a logic of programs in which compositional reasoning principles are formalized and proved sound with respect to trace semantics. The methods are illustrated through a small fragment of an idealized file system.

We consider an identity relating Fibonacci numbers to Pascal's triangle discovered by G. E. Andrews. Several authors provided proofs of this identity, most of them rather involved or else relying on sophisticated number theoretical arguments. We present a new proof, quite simple and based on a Riordan array argument. The main point of the proof is the construction of a new Riordan array from a given Riordan array, by the elimination of elements. We extend the method and as an application we obtain other identities, some of which are new. An important feature of our construction is that it establishes a nice connection between the generating function of the $A-$sequence of a certain class of Riordan arrays and hypergeometric functions., Comment: Accepted for publication in Discrete Mathematics