[TYPES/announce] Call for Participation: APLAS'11 (Asian Symposium on Programming Languages and Systems 2011) + CPP'11 (Certified Programs and Proofs 2011)

Tue Nov 1 16:00:55 EDT 2011

                  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