Basic Studies in Computing Science

主题：
计算机科学基础理论
Topic:
Summer School and Workshop on Basic Studies in Computer Science
时间：
2001年10月13日至14日 Workshop
2001年10月15日至19日 Summer School
地点：
中科院软件所
主办单位：
中科院软件所计算机科学实验室

顾问组：
Pierre-Louis Curien (Paris VII University)
Lin Huimin (Institute of Software, CAS)
Lu Ruqian (Institute of Mathematics, CAS)
Zhou Chaochen (International Institute for Software Technology, UNU)
程序委员会：
Cai Kaiyuan (Beijing University of Aeronautics and Astronautics)
Fu Yuxi (Shanghai Jiaotong University, Co-chair)
Jiang Changjun (Shanghai Tongji University)
Jin Zhi (Institute of Mathematics, CAS)
Li Zhoujun (National University of Defense Technology)
Lin Huimin (Institute of Software, CAS, Co-chair)
Lin Zuoquan (Beijing University)
Song Fangmin (Nanjing University)
Su Kaile (Zhongshang University)
Ying Mingsheng (Qinghua University)
Zhang Jian (Institute of Software, CAS)
组委会：
Chen Haiming (Institute of Software, CAS)
Guo Juqing (Institute of Software, CAS)
Jiang Ying (Institute of Software, CAS)
Hu Yongqian (Institute of Software, CAS)
Liu Xinxin (Institute of Software, CAS)

Pierre-Louis Curien: On the Symmetries of Computation
Abstract: We shall show, using tool from Gentzen's sequent calculus on one hand, and from Hyland-Ong style game semantics on the other hand (in the more abstract setting of the author's Abstract Boehm Trees), how deep symmetries of computation such as input/output or call-by-name/call-by-value can be expressed in a manifest way. This can be seen as an exercise on syntax design: semantics is not alien to syntax, it may be rather called a guide towards "essential syntax".
Thomas Ehrhard: Denotational Semantics of Linear Logic
Abstract: I will address two aspects of my recent work on denotational semantics.
DENOTATIONAL SEMANTICS and PHASE SEMANTICS. First, I will present a new way of building web-based denotational models of linear logic, based on a connection between denotational semantics and phase semantics. The idea is to associate a phase-valued coherence (and even indexed formulae of linear logic) to families of points of the webs of spaces. In this setting, the interpretation of the exponential is non-uniform. In particular, I will describe in full details a new version of the well-known coherence space semantics of linear logic obtained in that way. I will also discuss completeness issues in this setting. This is partly a work in common with Antonio, Bucciarelli (PPS, Paris).
DENOTATIONAL SEMANTICS and TOPOLOGICAL VECTOR SPACES. Then I will describe a model of linear logic in a restricted class of locally convex spaces, and more precisely of Kothe sequence spaces. In this setting, linear proofs are interpreted as linear continuous maps between spaces, and intuitionistic proofs are interpreted as entire maps (analytic maps defined by a power series converging on the whole space). I will discuss the extension of logic and lambda-calculus by differential privitives that this model suggests.
Cedric Fournet: The Join Calculus, a Language for Distributed and Mobile Programming
Abstract: I plan to give an overview of the join calculus, its model of distribution, and its equational theory.
The join calculus is a small language that models distributed, mobile programming. It is characterized by a notion of locality, a strict adherence to local synchronization, and a direct embedding of functional programming.
Locality and local synchronization mean that processes running at different locations interact with one another only by exchanging asynchronous messages (with set destinations), and that any other computation step involves a single location. This guarantees an efficient distributed implementation.
I will explain how concurrency theory can be applied to the join calculus, in order to state and prove correctness properties for programs and protocols written in the language.
I will also present and illustrate some mobility extensions of the language, which allow the programming of agent creation and agent mobility. I will finally present how the calculus has been extended to model distributed partial failures on the one hand, and security protocols on the other.
Jean-Yves Girard: LUDICS
Abstract: Since the late sixties, the end of the XXth century witnessed a revolution in logic that can be summarised by the slogan : FROM THE RULES OF LOGIC TO THE LOGIC OF RULES.
Logic is no longer about a preexistant external reality, but about its own protocols, its own geometry. Typically the negation is not about saying "NOT", but about the mirror, the duality "I" vs. "the world"... The new approach encompasses the old one, typically if "I" win, "the world" loses, i.e., wins "NOT". When logical artifacts are identified with their own rules of production, LOCATIVE phenomenons arise. In particular, one realises that usual logic (including linear logic) is SPIRITUAL, i.e., up to isomorphism. But there is a deeper locative level, with indeed a more regular structure. Typically the usual (additive) conjunction has the value of categorical product in usual logic, and enjoys commutativity, associativity, etc. up to isomorphism. In ludics, what corresponds is a plain intersection G \cap H, which is really associative, commutative, etc. (no isomorphisms)~; it contains the usual conjunction as a delocalised case \varphi(G) \cap \psi(H). The lectures will introduce to LUDICS, a monist presentation of logic ---without this nonsense distinction syntax/semantics/meta--- just plain logical artifacts, period, and expound the main properties, esp. the locative features.
Stefano Guerrini: Linear Logic: Sequent Calculus and Proof Nets
Abstract: We shall present the syntax of linear logic. Studying the sequent calculus, we shall discuss the reasons that lead to the splitting into multiplicative and additive connectives and to the introduction of exponentials. Then, we shall study proof-nets, the main syntactical novelty of linear logic.
John Reppy: Four Lectures on Moby
Abstract: Moby is an experimental language design that combines features from ML (modules, parametric polymorphism, datatypes, and higher-order functions) with class-based support for object-oriented programming and CML-style concurrency. It is meant to provide a testbed for language design ideas that might be incorporated into the design of ML2000.
Davide Sangiorgi: An Introduction to Process Calculi
Abstract: In the first part of the course I will introduce the basic concepts of process calculi, in particular that of behavioural equivalence, and briefly trace an history of the field. I will use examples written in the Calculus of Communicating Systems (CCS). Although CCS is very handy for a first exposure to the topic, its expressive power is rather limited. I will therefore move, in the second part of the course, to more a powerful process calculus, the pi-calculus.
The pi-calculus allows us, in particular, to describe mobile systems, that is, concurrent systems whose structure can change dynamically as the system evolves. This can happen, for instance, because some processes change location or because the visibility that a process has of the rest of the system (that is, the set of processes with which the given process can communicate) changes. We find mobility in many areas of computer science; for instance, operating systems, object-oriented programming, distributed systems.
The pi-calculus has emerged in recent years as one of the most influential of process calculi. I will present the pi-calculus viewing it both as a basic model of concurrent computations and as core programming language.

照片