Please see the Tutorials page for details.

• 09:00 - 12:00 Tutorial 1
  • Shin-Cheng Mu. Dependently Typed Programming in Adga.
• 12:00 - 14:00 Lunch (on your own)
• 14:00 - 17:00 Tutorial 2 (moved to 15:00 - 18:00, December 7)
  • Lei Liu. Parallelizing Legacy Sequential Code.

• 08:45 - 09:00 APLAS Opening
• 09:00 - 10:00 APLAS Invited talk
  • Sriram Rajamani. Program Analysis and Machine Learning: A Win-Win Deal.
• 10:00 - 10:30 Coffee break
• 10:30 - 12:30 APLAS Session 1 — Program Analysis.
  • David Monniaux and Martin Bodin. Modular Abstractions of Reactive Nodes using Disjunctive Invariants.
  • Thao Dang and Thomas Martin Gawlitza. Time Elapse over Template Polyhedra in Polynomial Time through Max-Strategy Iteration.
  • Hakjoo Oh and Kwangkeun Yi. Access-based Localization with Bypassing.
  • Fernando Saenz-Perez. A Deductive Database with Datalog and SQL Query Languages.
• 12:30 - 14:00 Lunch break
• 14:00 - 15:30 APLAS Session 2 — Functional Programming.
  • Yun-Yan Chi and Shin-Cheng Mu. Constructing List Homomorphisms from Proofs.
  • Dmitriy Traytel, Stefan Berghofer and Tobias Nipkow. Extending Hindley-Milner Type Inference with Coercive Subtyping.
  • Yuichiro Kokaji and Yukiyoshi Kameyama. Polymorphic Multi-Stage Language with Control Effects.
• 15:30 - 16:00 Coffee break
• 16:00 - 17:00 APLAS Session 3 — Compiler
  • 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.
  • Yulei Sui, Sen Ye, Jingling Xue and Pen-Chung Yew. SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA.

• 09:00 - 10:00 APLAS Invited talk
  • Ranjit Jhala. Software Verification with Liquid Types.
• 10:00 - 10:30 Coffee break
• 10:30 - 12:30 APLAS Session 4 — Concurrency 1
  • Alexander Malkis and Laurent Mauborgne. On the Strength of Owicki-Gries for Resources.
  • Ashutosh Gupta, Corneliu Popeea and Andrey Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF.
  • Akimasa Morihata. Macro Tree Transformations of Linear Size Increase Achieve Cost-optimal Parallelism.
  • Jonas Magazinius, Aslan Askarov and Andrei Sabelfeld. Decentralized Delimited Release.
• 12:30 - 14:00 Lunch break
• 14:00 - 15:30 APLAS Session 5 — Concurrency 2.
  • Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gomez-Zamalloa and German Puebla. Cost Analysis of Concurrent OO Programs.
  • Ana Milanova and Wei Huang. Static Object Race Detection.
  • Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal and Michael Tautschnig. Soundness of Data Flow Analyses for Weak Memory Models.
• 15:30 - 16:00 Coffee break
• 16:00 - 16:45 APLAS Poster session
• 16:45 - 17:45 APLAS Session 6 — Semantics.
  • Filippo Bonchi, Fabio Gadducci and Giacoma Monreale. Towards A General Theory of Barbs, Contexts and Labels.
  • Ulrich Schoepp. Computation-by-Interaction with Effects.

See the CPP homepage for the afternoon programme.

• 08:45 - 09:00 CPP Opening
• 09:00 - 10:00 APLAS+CPP Invited talk
  • Nikolaj Bjørner. Engineering Theories with Z3.
• 10:00 - 10:15 Coffee break
• 10:15 - 12:45 APLAS Session 7 — Certification and logic
  • Lukasz Fronc and Franck Pommereau. Towards a certified Petri net model-checker.
  • Patrick Baillot. Elementary linear logic revisited for polynomial time and an exponential time hierarchy.
  • 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.
  • Casey Klein, Jay Mccarthy, Steven Jaconette and Robert Bruce Findler. A Semantics for Context-Sensitive Reduction Semantics.
  • Zhen Cao, Yuan Dong and Shengyuan Wang. Compiler Backend Generation for Application Specific Instruction Set Processors.

• 12:30 - 14:00 Lunch break
• 14:00 - 15:00 APLAS+CPP Invited talk
  • Peter W. O'Hearn. Algebra, Logic, Locality, Concurrency.
• 15:00 - 16:00 CPP Session 1 (2 talks)
• 16:00 - 16:30 Coffee break
• 16:30 - 17:30 CPP Session 2 (2 talks)
• 17:30 - 18:15 CPP Session 3 (panel discussion)
• 19:00 - 21:00 APLAS+CPP Banquet

See the CPP homepage for detailed programme.

• 09:00 - 10:00 CPP Invited talk
  • Georges Gonthier. Proof engineering, from the four color to the Odd Order theorem.
• 10:00 - 10:30 Coffee break
• 10:30 - 12:30 CPP Session 4 (4 talks)
• 12:30 - 14:00 Lunch break
• 14:00 - 16:00 CPP Session 5 (4 talks)
• 16:00 - 16:30 Coffee break
• 16:30 - 17:30 CPP Session 6 (2 talks)

See the CPP homepage for detailed programme.

• 09:00 - 10:00 CPP Invited talk
  • Andrew Appel: VeriSmall: Verified Smallfoot Shape Analysis.
• 10:00 - 10:30 Coffee break
• 10:30 - 12:30 CPP Session 7 (4 talks)
• 12:30 - 14:00 Lunch break
• 14:00 - 15:30 CPP Session 8 (3 talks)
• 15:30 - 16:00 Coffee break
• 16:00 - 17:15 CPP Session 9 (2 talks + 1 short talk)