计算机科学中的逻辑

We study the complexity of a range of propositional proof systems which allow inference rules of the form: from a set of clauses $\Gamma$ derive the set of clauses $\Gamma \cup \{ C \}$ where, due to some syntactic condition, $\Gamma \cup…

A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the…

Proof theory provides a foundation for studying and reasoning about programming languages, most directly based on the well-known Curry-Howard isomorphism between intuitionistic logic and the typed lambda-calculus. More recently, a…

The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But…

Partially ordered automata are automata where the transition relation induces a partial order on states. The expressive power of partially ordered automata is closely related to the expressivity of fragments of first-order logic on finite…

We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number…

In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language - representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication - it is possible to…

We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is…

The notion of a complete Boolean algebra, although completely legitimate in constructive mathematics, fails to capture some natural structures such as the lattice of subsets of a given set. Sambin's notion of an overlap algebra, although…

We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the…

We develop a novel method to analyze the dynamics of stochastic rewriting systems evolving over finitary adhesive, extensive categories. Our formalism is based on the so-called rule algebra framework and exhibits an intimate relationship…

We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for…

One of the key aspects in component-based design is specifying the software architecture that characterizes the topology and the permissible interactions of the components of a system. To achieve well-founded design there is need to address…

We introduce a novel real-valued endogenous logic for expressing properties of probabilistic transition systems called Riesz modal logic. The design of the syntax and semantics of this logic is directly inspired by the theory of Riesz…

This paper presents a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. MSO on infinite trees is a rich system, and its decidability ("Rabin's Tree Theorem") is one of the most powerful known results…

Propositional team logic is the propositional analog to first-order team logic. Non-classical atoms of dependence, independence, inclusion, exclusion and anonymity can be expressed in it, but for all atoms except dependence only exponential…

The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple…

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types.…

The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its…

We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more…