TSD 2014
4th Tsinghua Software Day
               
 Home  Invited Speakers  Lectures  Program  Local Infomation  Contact Us  
               
Concurrent Constraint Programming: 25 years later by Vijay Saraswat

The basic ideas of Concurrent Constraint Programming (CCP) were introduced in 1987. At its heart, CCP is a simple but powerful declarative framework for concurrent programming, with deep ties to logic. Since 1987, the theory has been extended to account for synchronous computing (Timed CC), and discrete/continuous timed interactions (Hybrid CC). Additionally the subset of intuitionistic logic that can be understood in terms of concurrent processes and their testing has been significantly increased. Basic techniques for abstract interpretation and diagnosis have been developed. Implementations of different CCP languages have been developed.

This talk will survey the main technical developments of this field with the view of introducing the main ideas in as simple and accessible a way as possible.

The Challenges of Securing Systems Software by Greg Morrisett

Much of our computing infrastructure is still built using C and C++, in spite of overwhelming language-level problems that lead to security exploits. I will discuss a range of compiler-oriented techniques that researchers have explored to try and harden C/C++ systems code. In one corner, we have techniques such as Software Fault Isolation (SFI) that have low overhead, and guarantee to enforce a particular security policy. However, the SFI policy is relatively coarse-grained, and as such doesn't block important attacks. In another corner is the Secure Virtual Architecture (SVA) which enforces a fine-grained, object-level integrity policy comparable to type safety. However, SVA and related techniques can have high overhead for some code, and will generally break more programs than SFI. All of these techniques depend upon compiler transformations, optimizations, and/or analyses that could lead to a large trusted computing base (TCB). So I will also discuss recent research that helps to minimize the TCB via machine-checked proofs of correctness.

Quantum programming: From superposition of data to superposition of programs. by Mingsheng Ying

We propose a novel quantum programming paradigm - superposition-of-programs, motivated by the design idea of a popular class of quantum algorithms, namely quantum walk-based algorithms.

A new quantum programming language QGCL is defined to support the paradigm of superposition-of-programs. This language can be seen as a quantum extension of Dijkstra’s GCL (Guarded Command Language). Surprisingly, alternation in GCL splits into two different notions in the quantum setting: (1) classical alternation (of quantum programs) based on measurements, and (2) quantum alternation defined by external quantum "coins", with the latter being introduced in QGCL for the first time. Quantum alternation is the key program construct for realizing the paradigm of superposition-of-programs. Another very useful program construct in realizing the paradigm of superposition-of-programs, called quantum choice, can be easily defined in terms of quantum alternation. Furthermore, a kind of truly quantum recursion is then introduced.

The denotational semantics of QGCL are defined by introducing a new mathematical tool called the guarded composition of operator-valued functions. In particular, the semantics of quantum recursion can be properly defined by employing mathematical tools from second quantization, including Fock space and creation and annihilation operators.

We believe that quantum programming techniques in the superposition-of-programs paradigm will play an important role in further exploiting the unique power of quantum computing.

Types, Games and Higher-Order Programs. by Luke Ong

Higher-order model checking is the model checking of infinite trees that are generated by higher-order recursion schemes. Progress in higher-order model checking has combined ideas and methods from semantics (notably type theory and game semantics) with algorithmic techniques from automated verification and program analysis. This talk surveys recent advances in the development of efficient algorithms for higher-order model checking, and its applications to the verification of higher-order programs.