Program – APLAS 2016

8:50-9:00 Opening
9:00-10:00 Invited talk I
- Kazuaki Ishizaki (IBM Research — Tokyo)
  Making Hardware Accelerator Easier to Use
10:30-12:00 Verification and Analysis I (Session Chair: Sandrine Blazy)
- Sooyoung Cha, Sehun Jeong and Hakjoo Oh
  Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
- Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi and Priya Narasimhan
  AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
- Tatsuya Abe and Toshiyuki Maeda
  Observation-based Concurrent Program Logic for Relaxed Memory Consistency Models

12:00-13:00 Buffet Lunch
- 10th floor, Ta Quang Buu Building, Hanoi University of Science and Technology

13:30-14:30 Programming Paradigms (Session Chair: Walter Binder)
- Oleg Kiselyov
  Probabilistic Programming Language and its Incremental Evaluation
- Gabriel Radanne, Vincent Balat and Jérôme Vouillon
  Eliom: A core ML language for tierless Web programming
15:00-16:30 λ-calculus (Session Chair: Oleg Kiselyov)
- Taichi Yachi and Eijiro Sumii
  A Sound and Complete Bisimulation for Contextual Equivalence in λ-calculus with Call/cc
- Daniel J. Dougherty, Ugo De’ Liguoro, Luigi Liquori and Claude Stolze
  A Realizability Interpretation for Intersection and Union Types
- Beniamino Accattoli and Giulio Guerrieri
  Open Call-by-Value
17:00-18:00 Profiling and Debugging (Session Chair: Hidehiko Masuhara)
- Andrea Rosà, Lydia Y. Chen and Walter Binder
  AkkaProf: a Profiler for Akka Actors in Parallel and Distributed Applications
- Ryoya Arai, Shigeyuki Sato and Hideya Iwasaki
  A Debugger-Cooperative Higher-Order Contract System in Python

18:30-20:00 Welcome Reception
- Luc Thuy Restaurant, 16 Le Thai To Street, Hoan Kiem District, Hanoi

9:00-10:00 Invited talk II
- Frank Pfenning
  Substructural Proofs as Automata
10:30-12:00 Type Theory (Session Chair: Makoto Tatsuta)
- Furio Honsell, Marina Lenisa, Luigi Liquori and Ivan Scagnetto
  Implementing Cantor’s Paradise
- Yanpeng Yang, Xuan Bi and Bruno C. D. S. Oliveira
  Unified Syntax with Iso-Types
- Oleg Kiselyov, Yukiyoshi Kameyama and Yuto Sudo
  Refined Environment Classifiers: Type- and Scope-safe Code Generation with Mutable Cells

12:00-13:00 Buffet Lunch
- 10th floor, Ta Quang Buu Building, Hanoi University of Science and Technology

13:30-15:00 Verification and Analysis II (Session Chair: Wei Ngan Chin)
- Taku Terao, Takeshi Tsukada and Naoki Kobayashi
  Higher-Order Model Checking in Direct Style
- Azalea Raad, Aquinas Hobor, Philippa Gardner and Jules Villard
  Verifying Concurrent Graph Algorithms
- Kazuhide Yasukata, Takeshi Tsukada and Naoki Kobayashi
  Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation
15:00-16:30 Poster Session
16:30-18:00 Process Calculus (Session Chair: Eijiro Sumii)
- Alwen Tiu, Nam Nguyen and Ross Horne
  SPEC: An Equivalence Checker for Security Protocols
- Hans Hüttel
  Binary session types for psi-calculi
- Kai Stadtmüller, Martin Sulzmann and Peter Thiemann
  Static Trace-Based Deadlock Analysis for Synchronous Mini-Go
18:00-18:10 PC Chair Report

19:00-21:00 Banquet
- Ly Club, 4 Le Phung Hieu Street, Hoan Kiem District, Hanoi

9:00-10:00 Invited talk III
- Adam Chlipala
  Fiat: A New Perspective on Compiling Domain-Specific Languages in a Proof Assistant
10:30-12:00 Separation Logic (Session Chair: Xinyu Feng)
- Azalea Raad, José Fragoso Santos and Philippa Gardner
  DOM: Specification and Client Reasoning
- Makoto Tatsuta, Quang Loc Le and Wei-Ngan Chin
  Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
- Zhe Hou and Alwen Tiu
  Completeness for a First-order Abstract Separation Logic
12:00-12:10 Closing