[TYPES/announce] Call for Participation: APLAS+CPP

Thu Oct 20 21:34:09 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

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.