2016

We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability […]

We propose a new bi-intuitionistic type theory called Dualized Type Theory (DTT). It is a simple type theory with perfect intuitionistic duality, and corresponds to a single-sided polarized sequent calculus. We prove DTT strongly normalizing, and prove type preservation. DTT is based on a new […]

We study the semantic meaning of block structure using game semantics. To that end, we introduce the notion of block-innocent strategies and characterise call-by-value computation with block-allocated storage through soundness, finite definability and universality results. This puts us in a good […]

Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. For omega-regular winning conditions, it is known that such games can be solved in doubly-exponential time and that doubly-exponential lookahead is sufficient. […]

In this paper, we investigate the possibility of improvement of the widely-used filtering algorithm for the linear constraints in constraint satisfaction problems in the presence of the alldifferent constraints. In many cases, the fact that the variables in a linear constraint are also […]

We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. We work in an uninterpreted setting, where the meaning of the atomic actions is specified axiomatically using hypotheses of a certain form. Our […]

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by […]

Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on […]

We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents […]

We introduce Z-stability, a notion capturing the intuition that if a function f maps a metric space into a normed space and if the norm of f(x) is small, then x is close to a zero of f. Working in Bishop's constructive setting, we first study pointwise versions of Z-stability and the related notion […]

Constraint automata (CA) constitute a coordination model based on finite automata on infinite words. Originally introduced for modeling of coordinators, an interesting new application of CAs is implementing coordinators (i.e., compiling CAs into executable code). Such an approach […]

Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on […]

Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first. We present a natural deduction and a Curry-Howard correspondence for first-order and second-order Dummett's logic. We add to the lambda […]