On the geometry of intuitionistic S4 proofs.
Possible-worlds semantics for rule-based expert systems with set-valued weights
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...
Probabilistic operational semantics for the lambda calculus
Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin’s CPS translation is extended to accommodate the choice operator and shown correct with respect...
Propositional dynamic logic with recursive programs
Propositional Linear Temporal Logic with Initial Validity Semantics1
In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model...
Relational specifications
Resolution Methods in Proving the Program Correctness
Some results on complexity of μ-calculus evaluation in the black-box model
We consider μ-calculus formulas in a normal form: after a prefix of fixed-point quantifiers follows a quantifier-free expression. We are interested in the problem of evaluating (model checking) such formulas in a powerset lattice. We assume that the quantifier-free part of the expression can be any monotone function given by a black-box – we may only ask for its value for given arguments. As a first result we prove that when the lattice is fixed, the problem becomes polynomial (the assumption about...
The alternation hierarchy for the theory of -lattices.
Traced premonoidal categories
Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show that in a Freyd category, these notions are equivalent, generalizing a well-known theorem relating traces and Conway operators in cartesian categories.
Traced Premonoidal Categories
Motivated by some examples from functional programming, we propose a generalization of the notion of trace to symmetric premonoidal categories and of Conway operators to Freyd categories. We show that in a Freyd category, these notions are equivalent, generalizing a well-known theorem relating traces and Conway operators in Cartesian categories.
Информационные фреймы Барвайса и модальные логики.
Метод синтеза условий выводимости хорновских и некоторых других формул.
Насыщенное исчисление для хорновских секвенций полной линейной темпоральной логики первого порядка
Неподвижные точки модальных схем
О динамических теориях свободных алгебр
О системах алгоритмических алгерб, сохраняющих идеалы в решетке рекурсивно перечислимых множеств
Об одной недетерминированной программной логике