Valparaiso, Chile


Aarne Ranta
University of Gothenburg

Grammatical Framework tutorial.


Grammatical Framework (GF) is a grammar formalism based on type theory and functional programming. Type theory is used for defining language-independent semantic structures (abstract syntax), and functional programming for mapping these structures to different languages (concrete syntaxes). The resulting notion of multilingual grammars provides an efficient, declarative way to define translation systems and also to formally compare languages on different levels of abstraction. Comprehensive GF grammars have been built for more than 30 languages, by a world-wide open-source community of over 100 programmers.

The tutorial gives a hands-on introduction to GF. Its purpose is to enable the participants to build their own grammars as well as simple web applications for translation and grammar teaching. We will encourage participants to try out GF for their own languages and to invent their own applications of GF. For those who want to continue further, there is an endless space for contributing to the formalization of the grammars of the world and to a new generation of machine translation technologies.


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 (, 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.

Luca Vigano
King's College London

Symbolic Analysis of Internet Security Protocols and Services.


Experience over the last twentyfive years has shown that the design of protocols and services for Internet security is highly error-prone and that conventional validation techniques based on informal arguments and/or testing are not up to the task. It is now widely recognized that only formal analysis can provide the level of assurance required by both the developers and the users of the protocols and services. This is especially true not only when one considers the simple academic protocols that have been proposed as example applications for automated reasoning techniques and tools (such as the Needham-Schroeder Public Key Protocol and the like), but also when one tries to scale up these techniques and tools to industrial-strength Internet security protocols (like Kerberos, IKE, or TLS).

After a brief introduction to Internet security protocols and services, I will first survey some prominent techniques and tools for security protocol analysis, and then discuss in detail the techniques that underlie the symbolic on-the-fly model-checker OFMC, the AVANTSSAR Platform and the SPaCIoS Tool, three state-of-the-art tools for the analysis and testing of security protocol and services that I have been developing together with colleagues at various European institutions and companies. I will also highlight some of the success stories, i.e., the discovery of a number of new attacks and vulnerabilities on such protocols and services.


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.