All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 3 Next

Displaying 41 – 60 of 61

Showing per page

Probabilistic operational semantics for the lambda calculus

Ugo Dal Lago, Margherita Zorzi (2012)

RAIRO - Theoretical Informatics and Applications

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

Ugo Dal Lago, Margherita Zorzi (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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

Ugo Dal Lago, Margherita Zorzi (2012)

RAIRO - Theoretical Informatics and Applications

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 Linear Temporal Logic with Initial Validity Semantics1

Mariusz Giero (2015)

Formalized Mathematics

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...

Some results on complexity of μ-calculus evaluation in the black-box model

Paweł Parys (2013)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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...

Traced premonoidal categories

Nick Benton, Martin Hyland (2003)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

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

Nick Benton, Martin Hyland (2010)

RAIRO - Theoretical Informatics and Applications

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.

Currently displaying 41 – 60 of 61