Accepted Papers

  • Azalea Raad, José Fragoso Santos and Philippa Gardner
    DOM: Specification and Client Reasoning
  • Hans Hüttel
    Binary session types for psi-calculi
  • Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi and Priya Narasimhan
    AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code
  • Azalea Raad, Aquinas Hobor, Philippa Gardner and Jules Villard
    Verifying Concurrent Graph Algorithms
  • Makoto Tatsuta, Quang Loc Le and Wei-Ngan Chin
    Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
  • Furio Honsell, Marina Lenisa, Luigi Liquori and Ivan Scagnetto
    Implementing Cantor’s Paradise
  • Oleg Kiselyov
    Probabilistic Programming Language and its Incremental Evaluation
  • Alwen Tiu, Nam Nguyen and Ross Horne
    SPEC: An Equivalence Checker for Security Protocols
  • Gabriel Radanne, Vincent Balat and Jérôme Vouillon
    Eliom: A core ML language for tierless Web programming
  • Ryoya Arai, Shigeyuki Sato and Hideya Iwasaki
    A Debugger-Cooperative Higher-Order Contract System in Python
  • Sooyoung Cha, Sehun Jeong and Hakjoo Oh
    Learning a Strategy for Choosing Widening Thresholds from a Large Codebase
  • Taichi Yachi and Eijiro Sumii
    A Sound and Complete Bisimulation for Contextual Equivalence in $\lambda$-calculus with Call/cc
  • Zhe Hou and Alwen Tiu
    Completeness for a First-order Abstract Separation Logic
  • Yanpeng Yang, Xuan Bi and Bruno C. D. S. Oliveira
    Unified Syntax with Iso-Types
  • Kazuhide Yasukata, Takeshi Tsukada and Naoki Kobayashi
    Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation
  • Daniel J. Dougherty, Ugo De’ Liguoro, Luigi Liquori and Claude Stolze
    A Realizability Interpretation for Intersection and Union Types
  • Kai Stadtmüller, Martin Sulzmann and Peter Thiemann
    Static Trace-Based Deadlock Analysis for Synchronous Mini-Go
  • Tatsuya Abe and Toshiyuki Maeda
    Observation-based Concurrent Program Logic for Relaxed Memory Consistency Models
  • Taku Terao, Takeshi Tsukada and Naoki Kobayashi
    Higher-Order Model Checking in Direct Style
  • Oleg Kiselyov, Yukiyoshi Kameyama and Yuto Sudo
    Refined Environment Classifiers: Type- and Scope-safe Code Generation with Mutable Cells
  • Andrea Rosà, Lydia Y. Chen and Walter Binder
    AkkaProf: a Profiler for Akka Actors in Parallel and Distributed Applications
  • Beniamino Accattoli and Giulio Guerrieri
    Open Call-by-Value