Volume 12, Issue 3

2016


1. Reasoning about Data Repetitions with Counter Systems

Demri, Stephane ; Figueira, Diego ; Praveen, M.
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 […]

2. Dualized Simple Type Theory

Eades III, Harley ; Stump, Aaron ; McCleeary, Ryan.
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 […]

3. Block structure vs scope extrusion: between innocence and omniscience

Murawski, Andrzej S. ; Tzevelekos, Nikos.
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 […]

4. How Much Lookahead is Needed to Win Infinite Games?

Klein, Felix ; Zimmermann, Martin.
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. […]

5. Solving finite-domain linear constraints in presence of the $\texttt{alldifferent}$

Banković, Milan.
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 […]

6. Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism

Mamouras, Konstantinos.
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 […]

7. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

Clouston, Ranald ; Bizjak, Aleš ; Grathwohl, Hans Bugge ; Birkedal, Lars.
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 […]

8. Build your own clarithmetic I: Setup and completeness

Japaridze, Giorgi.
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 […]

9. Idempotents in intensional type theory

Shulman, Michael.
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 […]

10. Z-stability in Constructive Analysis

Bridges, Douglas ; Dent, James ; McKubre-Jordens, Maarten.
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 […]

11. Data optimizations for constraint automata

Jongmans, Sung-Shik T. Q. ; Arbab, Farhad.
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 […]

12. Build your own clarithmetic II: Soundness

Japaridze, Giorgi.
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 […]

13. On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC

Aschieri, Federico.
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 […]