**Date: Wednesday, June 29, 2011.**

**Place:** Dianxin Building House III, Room 404, Dongchuan Road, No 800, Shanghai Jiaotong University (Minhang campus).

**11:00 am - 12:00 am**

**Speaker: Yuxi Fu (Shanghai Jiaotong University)**

**Title: What is a Model Theory of Computer Science?**

**Abstract:** We will argue that there is a necessity a model theory of computer science. We outline such a theory and report some of the recent developments.

**1:30 pm - 2:30 pm**

**Speaker: Jean-Francois Monin (University Joseph Fourier and LIAMA**

**Beijing)**

**Title: Proofs in Type Theory with Coq**

**Abstract:** After recalling the theoretical framework implemented by the proof-assistant Coq, we show how it is used in practice in 2 actual and very different projects at LIAMA/FORMES. The fist is devoted to the study of distributed algorithms, while the second is about the certification of a large and efficient simulator of ARM-based embedded systems written in C. Some hints on the technical barriers to be overcome will be given.

**2:45 pm - 3:45 pm**

**Speaker: Anthony Widjaja Lin (Oxford University)**

**Title: Parikh Images of Regular Languages: Complexity and Applications**

**Abstract:** Parikh's Theorem is a fundamental result in automata theory stating that the Parikh images (i.e. the sets of letter

counts) of context-free languages and regular languages coincide with semilinear sets. Here, we provide results concerning descriptional and computational complexity of Parikh's Theorem. We show that the Parikh image of the language of an NFA with n states over an alphabet of size k can be described as a finite union of linear sets with at most k generators and total size polynomial for all *fixed* k >= 1. Previously, it was not known whether the number of generators could be made independent of n, and best upper bounds on the total size were exponential in n. Furthermore, we give an polynomial algorithm for performing such a translation for all fixed k \geq 1. Our proof exploits a connection with convex geometry and establishes a normal form theorem for semilinear sets. To complement these results, we show that our upper bounds are tight and that the results cannot be extended to context-free languages. The results have can be applied to obtain many different ``tractability''

results in several different areas in theoretical computer science (e.g. integer programming, graph databases, PAC-learning of semilinear sets, verification). Time permitting, I will discuss several of these applications.

**4:00pm - 5:00pm**

**Speaker: Zhengfeng Ji (Perimeter Institute for Theoretical Physics)**

**Title: Hamiltonian for Hamiltonian Path Problem**

**Abstract:** In this talk, I will survey some topics in quantum computing relating to the quantum generalization of NP, and more generally the new field of Hamiltonian complexity.