CALL FOR PARTICIPATION

                          APLAS+CPP
                       Kenting, Taiwan
                    December 4 to 9, 2011


APLAS aims at stimulating programming language research by providing a
forum for the presentation of latest results and the exchange of ideas
in topics concerned with programming languages and systems. APLAS is
based in Asia, but is an international forum that serves the worldwide
programming language community. 

CPP is a new international forum on theoretical and practical topics
in all areas, including computer science, mathematics, and education,
that consider certification as an essential paradigm for their
work. Certification here means formal, mechanized verification of some
sort, preferably with production of independently checkable
certificates. CPP targets any research promoting formal development of
certified software and proofs.

For the first time, APLAS and CPP will be held together in Kenting,
Taiwan from December 4 to 9, 2011. The six-day event includes two
tutorials, six invited talks, and two conferences. We offer a special
rate for participants who register to both conferences. For the
detailed program of each conference, please go to their respective web
sites:

http://flolac.iis.sinica.edu.tw/aplas11/doku.php  (APLAS)
http://formes.asia/cpp/                           (CPP)

Early Registration (until November 12, 2011)

             Regular   |   Student
-----------------------+-----------
APLAS+CPP:  TWD 24000  |  TWD 19500
APLAS only: TWD 16500  |  TWD 13500
CPP only:   TWD 16500  |  TWD 13500

Location

The conferences will be held in Kenting, a seaside resort and national
park in Southern Taiwan. Temperatures in Kenting averaged at 21.4 C in
December 2010 (high: 29.5, low: 14.3). It can be a bit windy, but the
weather probably is the best in Taiwan in December. You can find more
information about the Kenting National Park at Wikipedia and
Wikitravel. The conference venue is Howard Beach Resort Kenting.

Keynote Speakers

o Andrew Appel (Princeton University)
  VeriSmall: Verified Smallfoot Shape Analysis
o Nikolaj Bjorner (Microsoft Research)
  Engineering Theories with Z3
o Ranjit Jhala (UC San Diego)
  Software Verification with Liquid Types
o Peter O'Hearn (Queen Mary, University of London)
  Algebra, Logic, Locality, Concurrency
o Sriram Rajamani (Microsoft Research India)
  Program Analysis and Machine Learning: A Win-Win Deal
o Vladimir Voevodsky (Institute for Advanced Study, Princeton)
  Univalent Semantics of Constructive Type Theories

Tutorials

o Lei Liu (Chinese Academy of Sciences)
  Parallelizing Legacy Sequential Code
o Shin-Cheng Mu (Academia Sinica)
  Dependently Typed Programming in Adga

Panels

o Certificates (moderator: Dale Miller)
o Teaching with Proof Assistants (moderator: Tobias Nipkow)

List of Accepted Papers

APLAS

o Thao Dang and Thomas Martin Gawlitza. Time Elapse over Template
  Polyhedra in Polynomial Time through Max-Strategy Iteration
o David Monniaux and Martin Bodin. Modular Abstractions of Reactive
  Nodes using Disjunctive Invariants 
o Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa and
  German Puebla. Cost Analysis of Concurrent OO Programs 
o Benoit Boissinot, Florian Brandner, Alain Darte, Benoit Dupont De
  Dinechin and Fabrice Rastello. A Non-Iterative Data-Flow Algorithm for
  Computing Liveness Sets in Strict SSA Programs 
o Dmitriy Traytel, Stefan Berghofer and Tobias Nipkow. Extending
  Hindley-Milner Type Inference with Coercive Subtyping 
o Patrick Baillot. Elementary linear logic revisited for polynomial
  time and an exponential time hierarchy 
o Zhen Cao, Yuan Dong and Shengyuan Wang. Compiler Backend Generation
  for Application Specific Instruction Set Processors 
o Akimasa Morihata. Macro Tree Transformations of Linear Size Increase
  Achieve Cost-optimal Parallelism 
o Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal and
  Michael Tautschnig. Soundness of Data Flow Analyses for Weak Memory
  Models 
o Yulei Sui, Sen Ye, Jingling Xue and Pen-Chung Yew. SPAS: Scalable
  Path-Sensitive Pointer Analysis on Full-Sparse SSA 
o Keiko Nakata, Tarmo Uustalu and Marc Bezem. A Proof Pearl with the
  Fan Theorem and Bar Induction: Walking through Infinite Trees with
  Mixed Induction and Coinduction 
o Ulrich Schoepp. Computation-by-Interaction with Effects 
o Ashutosh Gupta, Corneliu Popeea and Andrey Rybalchenko. Solving
  Recursion-Free Horn Clauses over LI+UIF 
o Hakjoo Oh and Kwangkeun Yi. Access-based Localization with Bypassing 
o Yun-Yan Chi and Shin-Cheng Mu. Constructing List Homomorphisms from
  Proofs 
o Jonas Magazinius, Aslan Askarov and Andrei Sabelfeld. Decentralized
  Delimited Release 
o Filippo Bonchi, Fabio Gadducci and Giacoma Monreale. Towards A
  General Theory of Barbs, Contexts and Labels 
o Lukasz Fronc and Franck Pommereau. Towards a Certified Petri Net
  Model-Checker 
o Fernando Saenz-Perez. A Deductive Database with Datalog and SQL
  Query Languages
o Yuichiro Kokaji and Yukiyoshi Kameyama. Polymorphic Multi-Stage
  Language with Control Effects 
o Ana Milanova and Wei Huang. Static Object Race Detection
o Alexander Malkis and Laurent Mauborgne. On the Strength of
  Owicki-Gries for Resources 
o Casey Klein, Jay Mccarthy, Steven Jaconette and Robert Bruce
  Findler. A Semantics for Context-Sensitive Reduction Semantics 

CPP

o Mathieu Boespflug, Maxime Dénès and Benjamin Grégoire. Full
  reduction at full throttle 
o Thi Minh Tuyen Nguyen and Claude Marché. Hardware-Dependent Proofs
  of Numerical Programs 
o Dongchen Jiang and Tobias Nipkow. Proof Pearl: The Marriage Theorem 
o Jean-David Genevaux, Julien Narboux and Pascal
  Schreck. Formalization of Wu's simple method in Coq 
o Thomas Braibant. Coquet: a Coq library for verifying hardware
o Martin Henz and Aquinas Hobor. Teaching Logic and Formal Methods
  with Coq 
o Christian Doczkal and Gert Smolka. Constructive Formalization of
  Hybrid Logic with Eventualities 
o Sorin Stratulat and Vincent Demange. Automated Certification of
  Implicit Induction Proofs 
o Michael Armand, Germain Faure, Benjamin Gregoire, Chantal Keller,
  Laurent Théry and Benjamin Werner. A Modular Integration of SAT/SMT
  Solvers to Coq through Proof Witnesses 
o Jinjiang Lei and Zongyan Qiu. Verification of Scalable Synchronous Queue 
o Thomas Braibant and Damien Pous. Tactics for Reasoning modulo AC in Coq 
o Tom Ridge. Simple, functional, sound and complete parsing for all
  context-free grammars 
o Thierry Coquand and Vincent Siles. A Decision Procedure for Regular
  Expression Equivalence in Type Theory 
o Pierre Corbineau, Mathilde Duclos and Yassine Lakhnech. Certified
  Security Proofs of Cryptographic Protocols in the Computational
  Model : an Application to Intrusion Resilience 
o Jieung Kim and Sukyoung Ryu. Coq Mechanization of Featherweight
  Fortress with Multiple Dispatch and Multiple Inheritance 
o Xiaomu Shi, Jean-Francois Monin, Frédéric Tuong and Frédéric
  Blanqui. First Steps Towards the Certification of an ARM Simulator 
o Sascha Böhme, Anthony Fox, Thomas Sewell and Tjark
  Weber. Reconstruction of Z3's Bit-Vector Proofs in HOL4 and
  Isabelle/HOL 
o Cezary Kaliszyk and Henk Barendregt. Reasoning about Constants in
  Nominal Isabelle, or how to Formalize the Second Fixed Point Theorem 
o Frédéric Besson, Pierre-Emmanuel Cornilleau and David
  Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq 
o Luis Caires, Frank Pfenning and Bernardo Toninho. Proof-Carrying
  Code in a Session-Typed Process Calculus 
o Wolfram Kahl. CalcCheck: A Proof Checker for Gries and Schneider's
  "Logical Approach to Discrete Math" 
o James Cheney and Christian Urban. Mechanizing the metatheory of
  mini-XQuery 
o Dale Miller. A proposal for broad spectrum proof certificates 
o Michael Backes, Catalin Hritcu and Thorsten Tarrach. Automatically
  Verifying Typing Constraints for a Data Processing Language