ﻻ يوجد ملخص باللغة العربية
Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural induction and structural recursion. However, for graphs or tree-like structures - trees involving cycles and sharing - it remains unclear what kind of inductive structures exists and how we can faithfully assign a term representation of them. In this paper we propose a simple term syntax for cyclic sharing structures that admits structural induction and recursion principles. We show that the obtained syntax is directly usable in the functional language Haskell and the proof assistant Agda, as well as ordinary data structures such as lists and trees. To achieve this goal, we use a categorical approach to initial algebra semantics in a presheaf category. That approach follows the line of Fiore, Plotkin and Turis models of abstract syntax with variable binding.
This paper extends a standard process algebra with a time-out operator, thereby increasing its absolute expressiveness, while remaining within the realm of untimed process algebra, in the sense that the progress of time is not quantified. Trace and f
This paper introduces the counterpart of strong bisimilarity for labelled transition systems extended with time-out transitions. It supports this concept through a modal characterisation, congruence results for a standard process algebra with recursion, and a complete axiomatisation.
The primary goal of this paper is to present a unified way to transform the syntax of a logic system into certain initial algebraic structure so that it can be studied algebraically. The algebraic structures which one may choose for this purpose are
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the
Types in logic programming have focused on conservative approximations of program semantics by regular types, on one hand, and on type systems based on a prescriptive semantics defined for typed programs, on the other. In this paper, we define a new