Valparaiso, Chile

- Verónica Becher (Universidad de Buenos Aires)
- Juha Kontinen (University of Helsinki)
- Aarne Ranta (University of Gothenburg)
- Kazushige Terui (Kyoto University)
- Luca Vigano (King's College London)
- Thomas Wilke (Christian-Albrechts-Universität zu Kiel)

Universidad de Buenos Aires & CONICET

Talk:

On Normal Numbers.
Normality is a weak form of randomness. A real number is simply normal to a given base if each digit occurs in the expansion with the same limit frequency. A real number is normal to a given base if each block of digits of equal length occurs in the expansion with the same limit frequency. And it is absolutely normal if it is normal to all bases. This definition was introduced by Émile Borel more than one hundred years ago, but not much is known about normal numbers. One of the famous open problems is whether the usual mathematical constants, as \pi, e and \sqrt{2}, are simply normal to any base. In this talk I will summarize some recent results on normal numbers that answer the following questions: How does simple normality to one base relates to simple normality to other bases? How does normality to one base relates to normality to other bases? How does normality to a given base relates to compressibility on different automata? How can we efficiently compute the expansion of an absolutely normal number? How can we construct absolutely normal Liouville numbers? The proofs integrate logical, combinatorial and number-theoretic tools.

** Verónica Becher ** is Associate Professor at the University of Buenos Aires,
researcher at CONICET Argentina, and member of the Laboratoire International
Associé INFINIS CONICET-UBA/CNRS-Université Paris Diderot.
Her research is in algorithmic randomness, Kolmogorov complexity
and problems on words. She is particularly interested in
the most elementary form of randomness for real numbers,
the property of normality.
More information here .

University of Helsinki

Talk:

Dependence Logic.
Dependence logic, introduced by Jouko Väänänen in 2007, is a new logic incorporating the concept of dependence into first-order logic. In the past few years, the team semantics of dependence logic has grown into a new framework in which various notions of dependence and independence can be formalized and studied. We review recent results on dependence logic and its applications.

** Juha Kontinen ** works as a Finnish Academy Research Fellow at the Department of
Mathematics and Statistics of the University of Helsinki.
He received his Ph.D.from the University of Helsinki in 2005.
He works in the areas of dependence logic, finite model theory,
and logic in computer science.

University of Gothenburg

Talk:

Syntax and Semantics for Translation.
Translation is expected to preserve the semantics of the source text and produce correct syntax in the target language. Obvious as this is for human translators, machine translation usually involves shortcuts that compromise both of these requirements. In this talk, we will take a look at what is needed to fulfil them. In particular, we will see how formal grammars should be written in order to help translation preserve semantics. The syntax and semantics that result are in many ways different from grammars that are written in a monolingual perspective. The question has its roots in the old ideas of a Universal Grammar, and has in modern times been suggested by Curry. Translation-oriented grammars were put to use in the Rosetta system at Philips in the 1980's, and are used today in the Grammatical Framework (GF). This talk will start from the basic concepts of syntax, semantics, and translation, and end up discussing some recent developments in GF.

** Aarne Ranta ** is Professor of Computer Science at the
University of Gothenburg and CEO of the start-up company Digital Grammars.
His early theoretical work on constructive type theory and natural language
(Type Theoretical Grammar, OUP 1994) led him to create the grammar formalism GF
(www.grammaticalframework.org), which has been used by a world-wide
community to build computational grammars for over 30 languages. In the last
five years, Ranta's main interest has been machine translation, where GF is
used for domain-specific high-quality systems. His current focus is on
extending the coverage of translation without losing control of its
quality.

Kyoto University

Talk:

Intersection types for normalization and verification.
One of the basic principles in typed lambda calculi is that typable lambda
terms are
normalizable. Since the converse direction does not hold for simply typed
lambda calculus,
people have been studying its extensions. This gave birth to the
intersection type systems,
that exactly characterize various classes of lambda terms, such as
strongly/weakly
normalizable terms and solvable ones.

There is another, more recent trend: intersection types are not only useful
for
extending simple types but also for refining them. One thus obtains finer
information on
simply typed terms by assigning intersection types. This in particular leads
to the concept of
normalization by typing, that turns out to be quite efficient in some
situations. Moreover,
intersection types are invariant under beta-eta equivalence (when assigned
to simply typed terms),
so that they constitute a denotational semantics (the Scott model of linear
logic),
that provides a seemingly more direct interpretation of lambda terms
than the traditional filter model. Finally, intersection types also work in
an infinitary setting,
where terms may represent infinite trees and types play the role of
automata.
This leads to a model checking framework for higher order recursion schemes
via intersection types (developed by Kobayashi and Ong).

The purpose of this talk is to outline the recent development of
intersection types
described above. In particular, we explain how an efficient evaluation
algorithm
is obtained by combining normalization by typing, beta-reduction and
Krivine?s
abstract machine, to result in the following complexity characterization.
Consider simply typed lambda terms of boolean type and of order r.
Then the problem of deciding whether a given term evaluates
to ?true? is complete for n-EXPTIME if r = 2n + 2, and complete for
n-EXPSPACE if
r = 2n + 3.

**Kazushige Terui** is an associate professor at Research Institute for Mathematical
Sciences, Kyoto University. His research interest lies in nonclassical logics for
theoretical computer science. In particular, he has been working on linear logic and
substructural logics with applications to implicit computational complexity
and ordered algebra.

King's College London

Talk:

Modal and temporal deduction systems for quantum state transformations.
Modal and temporal logics have proven suitable to formally represent and reason about transformations of quantum states in an abstract, qualitative, way. Quantum states represent quantum systems, and can be viewed as the structure of quantum data for quantum operations. In this talk, I will first introduce a modal framework for reasoning about operations on quantum states (unitary transformations and measurements) in terms of possible worlds (as abstractions of quantum states) and accessibility relations between these worlds. Then, I will present the Distributed Temporal Logic DTL, which allows one to reason about temporal properties of a distributed system from the local point of view of the system’s agents, which are assumed to execute independently and to interact by means of event sharing. I will introduce the Quantum Distributed (Branching) Temporal Logic QDTL, a variant of DTL able to represent quantum state transformations in a more satisfactory way than simple modal systems. In QDTL, each agent represents a distinct quantum bit (the unit of quantum information theory), which evolves by means of quantum transformations and possibly interacts with other agents. n-ary quantum operators act as communication/synchronization points between agents. QDTL is endowed with a DTL-style semantics, which fits the intrinsically distributed nature of quantum computing. Finally, I will discuss possible extensions in order to reason about entanglement phenomena. Joint work with Andrea Masini, Marco Volpe, Margherita Zorzi.

Prof. Dr. ** Luca Viganò ** received his Ph.D. in Computer Science from
the University of Saarbruecken, Germany, in 1997, and his Habilitation in
Computer Science from the University of Freiburg, Germany, in 2003.
He held a senior research scientist position at ETH Zurich, Switzerland,
from January 2003 to October 2006, and was then an Associate Professor of
Computer Science at the University of Verona, Italy, until October 2013.
He is now full professor of Computer Science (Software Modelling and Applied Logic)
at King's College London, UK. His research focuses on formal methods and
tools for the specification, verification, and construction of secure systems,
and on the theory and applications of non-classical and security logics.

Christian-Albrechts-Universität zu Kiel

Talk:

Backward deterministic Büchi automata.
Backward deterministic Büchi automata were introduced by Olivier Carton and Max Michel in the late nineties. In the talk, an overview over the theory of backward deterministic Büchi automata is given.

** Thomas Wilke ** holds a diploma in computer science from
RWTH Aachen, and received a Ph.D. in computer science from Kiel University in 1994.
As a post-doc, he worked at DIMACS (Rutgers University),
RWTH Aachen, and Kiel University; he visited the University of Bordeaux,
ENS Cachan, and the University of Marne-la-Valleé.
He is professor of computer science since 1999.
His areas of interest are logic in computer science, automata theory,
and cryptographic protocols.