Sciweavers

Share
FOSSACS
2016
Springer
4 years 4 months ago
Synchronizing Automata over Nested Words
Abstract. We extend the concept of a synchronizing word from finitestate automata (DFA) to nested word automata (NWA): A well-matched nested word is called synchronizing if it res...
Dmitry Chistikov, Pavel Martyugin, Mahsa Shirmoham...
FOSSACS
2016
Springer
4 years 4 months ago
Contextual Approximation and Higher-Order Procedures
We investigate the complexity of deciding contextual approximation (refinement) in finitary Idealized Algol, a prototypical language combining higherorder types with state. Earli...
Ranko Lazic, Andrzej S. Murawski
FOSSACS
2016
Springer
4 years 4 months ago
Unary Resolution: Characterizing Ptime
We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring (whose elements can be understood as logic pr...
Clément Aubert, Marc Bagnol, Thomas Seiller
FOSSACS
2016
Springer
4 years 4 months ago
A Coalgebraic View of Bar Recursion and Bar Induction
We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover ...
Venanzio Capretta, Tarmo Uustalu
FOSSACS
2016
Springer
4 years 4 months ago
Join Inverse Categories as Models of Reversible Recursion
Recently, a number of reversible functional programming languages have been proposed. Common to several of these is the assumption of totality, a property that is not necessarily d...
Holger Bock Axelsen, Robin Kaarsgaard
FOSSACS
2016
Springer
4 years 4 months ago
On Freeze LTL with Ordered Attributes
This paper is concerned with Freeze LTL, a temporal logic on data words with registers. In a (multi-attributed) data word each position carries a letter from a finite alphabet and...
Normann Decker, Daniel Thoma
FOSSACS
2016
Springer
4 years 4 months ago
Reasoning About Call-by-need by Means of Types
Abstract. We first develop a (semantical) characterization of call-byneed normalization by means of typability, i.e. we show that a term is normalizing in call-by-need if and only...
Delia Kesner
FOSSACS
2016
Springer
4 years 4 months ago
Qualitative Analysis of VASS-Induced MDPs
We consider infinite-state Markov decision processes (MDPs) that are induced by extensions of vector addition systems with states (VASS). Verification conditions for these MDPs a...
Parosh Aziz Abdulla, Radu Ciobanu, Richard Mayr, A...
FOSSACS
2016
Springer
4 years 4 months ago
Regular Transformations of Data Words Through Origin Information
We introduce a class of transformations of finite data words generalizing the well-known class of regular finite string transformations described by MSO-definable transductions ...
Antoine Durand-Gasselin, Peter Habermehl
FOSSACS
2016
Springer
4 years 4 months ago
Focused and Synthetic Nested Sequents
Focusing is a general technique for transforming a sequent proof system into one with a syntactic separation of non-deterministic choices without sacrificing completeness. This no...
Kaustuv Chaudhuri, Sonia Marin, Lutz Straßbu...
books