Programming Languages and Systems: 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010 Proceedings

by Kazunori Ueda (Editor)

Overview

The 23 papers presented together with 4 invited papers 2 system and tool presentations and 1 tutorial lecture were carefully reviewed and selected from 95 initial submissions. The papers are devoted to both foundational and practical issues in programming languages and systems and feature current research in the following areas: semantics, logics, foundational theory, design of languages and foundational calculi, type systems, compilers, interpreters, abstract machines, program derivation, analysis, transformation, software security, safety, verification, concurrency, constraints, domain-specific languages, as well as tools for programming, verification, and implementation.

Product Details

ISBN-13:	9783642171635
Publisher:	Springer Berlin Heidelberg
Publication date:	01/19/2011
Series:	Lecture Notes in Computer Science , #6461
Edition description:	2010
Pages:	440
Product dimensions:	0.00(w) x 0.00(h) x 0.04(d)

Table of Contents

Invited Talks

A Calculus for Hybrid CSP Jiang Liu Jidong Lu Zhao Quan Naijun Zhan Hengjun Zhao Chaochen Zhou Liang Zou 1

Foundations of Quantum Programming (Extended Abstract) Mingsheng Ying 16

From a Verified Kernel towards Verifed Systems Gerwin Klein 21

Reasoning about Computations Using Two-Levels of Logic Dale Miller 34

Session 1

Typechecking Higher-Order Security Libraries Karthik Bhargavan Cédric Fournet Nataliya Guts 47

Towards Deriving Type Systems and Implementations for Coroutines Konrad Anton Peter Thiemann 63

Liberal Typing for Functional Logic Programs Francisco López-Fraguas Enrique Martin-Martin Juan Rodríguez-Hortalá 80

Session 2

A Provably Correct Stackless Intermediate Representation for Java Bytecode Delphine Demange Thomas Jensen David Pichardie 97

JNI Light: An Operational Model for the Core JNI Gang Tan 114

An Interactive Tool for Analyzing Embedded SQL Queries Aivar Annamaa Andrey Breslav Jevgeni Kabanov Varmo Vene 131

Session 3

Simple and Precise Widenings for H-Polyhedra Axel Simon Liqian Chen 139

Metric Spaces and Termination Analyses Aziem Chawdhary Hongseok Yang 156

Session 4

Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics Jan Hoffmann Martin Hofmann 172

Interprocedural Control Flow Reconstruction Andrea Flexeder Bogdan Mihaila Michael Petter Helmut Seidl 188

Data Structure Fusion Peter Hawkins Alex Aiken Kathleen Fisher Martin Rinard Mooly Sagiv 204

Session 5

Categorical Descriptional Composition Shin-ya Katsumata 222

Bisimulation Proof Methods in a Path-Based Specification Language for Polynomial Coalgebras Xiao-cong Zhou Yong-ji Li Wen-jun Li Hai-yan Qiao Zhong-mei Shu 239

Context-Preserving XQuery Fusion Hiroyuki Kato Soichiro Hidaka Zhenjiang Hu Keisuke Nakano Yasunori Ishihara 255

Session 6

Index-Compact Garbage Collection Liangliang Tong Francis C.M. Lau 271

Live Heap Space Bounds for Real-Time Systems Martin Kero Pawel Pietrzak Johan Nordlander 287

Session 7

A Quick Tour of the VeriFast Program Verifier Bart Jacobs Jan Smans Frank Piessens 304

Verification of Tree-Processing Programs via Higher-Order Model Checking Hiroshi Unno Naoshi Tabuchi Naoki Kobayashi 312

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates Soonho Kong Yungbum Jung Cristina David Bow-Yaw Wang Kwangkeun Yi 328

Session 8

Relational Parametricity for a Polymorphic Linear Lambda Calculus Jianzhou Zhao Qi Zhang Steve Zdancewic 344

A Certified Implementation of ML with Structural Polymorphism Jacques Garrigue 360

Type Inference for Sublinear Space Functional Programming Ugo Dal Lago Ulrich Schöpp 376

Session 9

Liveness of Communicating Transactions (Extended Abstract) Edsko de Vries Vasileios Koutavas Matthew Hennessy 392

Model Independent Order Relations for Processes Chaodong He 408

Concurrency Can't Be Observed, Asynchronously Paolo Baldan Filippo Bonchi Fabio Gadducci Giacoma Valentina Monreale 424

Tutorial

A Logical Mix of Approximation and Separation Aquinas Hobor Robert Dockins Andrew W. Appel 439

Author Index 455