Search

• < Previous
• 1
• Next >

---

Representations of Stream Processors Using Nested Fixed Points

Neil Ghani ; Peter Hancock ; Dirk Pattinson.

We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions. We define also an operation on the representations of two continuous functions between streams that yields a&nbsp;[&hellip;]

---

EXPTIME Tableaux for the Coalgebraic mu-Calculus

Corina Cirstea ; Clemens Kupke ; Dirk Pattinson.

The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of&nbsp;[&hellip;]

---

Generic Modal Cut Elimination Applied to Conditional Logics

Dirk Pattinson ; Lutz Schröder.

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal&nbsp;[&hellip;]

---

Model Theory and Proof Theory of Coalgebraic Predicate Logic

Tadeusz Litak ; Dirk Pattinson ; Katsuhiko Sano ; Lutz Schröder.

We propose a generalization of first-order logic originating in a neglected work by C.C. Chang: a natural and generic correspondence language for any types of structures which can be recast as Set-coalgebras. We discuss axiomatization and completeness results for several natural classes of such&nbsp;[&hellip;]

---

Constructive Domains with Classical Witnesses

Dirk Pattinson ; Mina Mohammadian.

We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain&nbsp;[&hellip;]

---

Modal meet-implication logic

Jim de Groot ; Dirk Pattinson.

We extend the meet-implication fragment of propositional intuitionistic logic with a meet-preserving modality. We give semantics based on semilattices and a duality result with a suitable notion of descriptive frame. As a consequence we obtain completeness and identify a common (modal) fragment of a&nbsp;[&hellip;]

---