Valparaiso, Chile

Invited Speakers

Verónica Becher
Universidad de Buenos Aires & CONICET

Talk:
On Normal Numbers.

Abstract:

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.

Bio:

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 .

Juha Kontinen
University of Helsinki

Talk:
Dependence Logic.

Abstract:

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.

Bio:

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.

Aarne Ranta
University of Gothenburg

Talk:
Syntax and Semantics for Translation.

Abstract:

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.

Bio:

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.

Kazushige Terui
Kyoto University

Talk:
Intersection types for normalization and verification.

Abstract:

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.

Bio:

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.

Luca Vigano
King's College London

Talk:
Modal and temporal deduction systems for quantum state transformations.

Abstract:

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.

Bio:

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.

Thomas Wilke
Christian-Albrechts-Universität zu Kiel

Talk:
Backward deterministic Büchi automata.

Abstract:

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.

Bio:

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.