In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation ofprograms into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also inthe presence of imperative features. This is made possible by considering a natural translation of Static Single Assignment intermediate form programs into Horn formulas, where φ functionscorrespond to union types.

The calculus of looping sequences is a formalism for describing theevolution of biological systems by means of term rewriting rules. Inthis paper we enrich this calculus with a type discipline whichpreserves some biological properties depending on the minimum andthe maximum number of elements of some type requested by the present elements. The typesystem enforces these properties and typed reductions guarantee thatevolution preserves them. As an example, we model the hemoglobinstructure and the equilibrium between cell death and division: typedreductions prevent undesirable behaviors.

Minimizing a deterministic finite automata (DFA) is a very important problem in theory of automata and formal languages.Hopcroft's algorithm represents the fastest known solution to the such a problem. In this paper we analyze the behavior of this algorithm on a family binary automata, called tree-like automata, associated to binary labeled trees constructed by words. We prove that all the executions of the algorithm on tree-like automata associated to trees, constructed by standard words, have running time with the same asymptotic growth rate. In particular, we provide a lower and upper bound for the running time of the algorithm expressed in terms of combinatorial properties of the trees. We consider also tree-like automata associated to trees constructed by de Brujin words,and we prove that a queue implementation of the waiting set gives a Θ(n log n) execution while a stack implementation produces a linear execution. Such a result confirms the conjecture given in [A. Paun, M. Paun and A. Rodríguez-Patón. Theoret. Comput. Sci.410 (2009) 2424–2430.] formulated for a family of unary automata and, in addition, gives a positive answer also for the binary case.

An ever present, common sense idea in language modelling research is that, for aword to be a valid phrase, it should comply with multiple constraints atonce. A new language definition model is studied, based on agreement or consensusbetween similar strings. Considering a regular set of strings over a bipartitealphabet made by pairs of unmarked/marked symbols, a match relation isintroduced, in order to specify when such strings agree. Then a regular setover the bipartite alphabet can be interpreted as specifying another languageover the unmarked alphabet, called the consensual language. A word is in theconsensual language if a set of corresponding matching strings is in theoriginal language. The family thus defined includes the regular languages andalso interesting non-semilinear ones. The word problem can be solved inNLOGSPACE, hence in P time. The emptiness problem is undecidable. Closure properties areproved for intersection with regular sets and inverse alphabetical homomorphism.Several conditions for a consensual definition to yield a regular language arepresented, and it is shown that the size of a consensual specification ofregular languages can be in a logarithmic ratio with respect to a DFA. Thefamily is incomparable with context-free and tree-adjoining grammar families.

Quantum annealing, or quantum stochastic optimization, is a classical randomized algorithm which provides good heuristics for the solution of hard optimization problems. The algorithm, suggested by the behaviour of quantum systems, is an example of proficuous cross contamination between classical and quantum computer science. In this survey paper we illustrate how hard combinatorial problems are tackled by quantum computation and present some examples of the heuristics provided by quantum annealing. We also present preliminary results about the application of quantum dissipation (as an alternative to imaginary time evolution) to the task of driving a quantum system toward its state of lowest energy.

We add sequential operations to the categorical algebra of weighted andMarkov automata introduced in [L. de Francesco Albasini, N. Sabadini and R.F.C. Walters, 
arXiv:0909.4136]. The extra expressiveness of the algebra permits the description of hierarchical systems, and ones withevolving geometry. We make a comparison with the probabilistic automata of Lynch et al. [SIAM J. Comput.37 (2007) 977–1013].

We extend the simply typedλ-calculus with unbind and rebind primitiveconstructs. That is, a value can be a fragment of open code,which in order to be used should be explicitly rebound. Thismechanism nicely coexists with standard static binding. Themotivation is to provide an unifying foundation for mechanisms ofdynamic scoping, where the meaning of a name isdetermined at runtime, rebinding, such as dynamic updatingof resources and exchange of mobile code, and delegation,where an alternative action is taken if a binding is missing.Depending on the application scenario, we consider twoextensions which differ in the way type safety is guaranteed. Theformer relies on a combination of static and dynamic type checking.That is, rebind raises a dynamic error if for some variablethere is no replacing term or it has the wrong type. In the latter,this error is prevented by a purely static type system, at the priceof more sophisticated types.

Wang automata are devices for picture language recognition recently introduced by us, which characterize the class REC of recognizable picture languages. Thus, Wang automata are equivalent to tiling systems or online tessellation acceptors, and are based like Wang systems on labeled Wang tiles. The present work focus on scanning strategies, to prove that the ones Wang automata are based on are those following four kinds of movements: boustrophedonic, “L-like”, “U-like”, and spirals.