Accepted Papers


  • Satoshi Egi and Yuichi Nishiwaki, Non-linear Pattern Matching with Backtracking for
    Non-free Data Types
  • Youssef El Bakouny and Dany Mezher.  Scallina: Translating Verified Programs from Coq to Scala
  • Pablo Barenbaum and Gonzalo Ciruelos. Factoring Derivation Spaces via Intersection Types
  • Mingzhang Huang, Hongfei Fu and Krishnendu Chatterjee. New Approaches for Almost-Sure Termination of Probabilistic Programs
  • Li Sui, Jens Dietrich, Amjed Tahir, Shawn Rasheed and Michael Emery. On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features – A Benchmark and Tool Evaluation
  • Taro Sekiyama and Kohei Suenaga. Automated proof synthesis for the minimal propositional logic with deep neural networks
  • Urara Yamada and Kenichi Asai. Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS
  • Depeng Liu, Bow-Yaw Wang and Lijun Zhang. Model Checking Differentially Private Properties
  • Adrien Champion, Naoki Kobayashi and Ryosuke Sato. HoIce: A ICE-based Non-Linear Horn Clause Solver
  • Junpeng Zha, Xinyu Feng and Lei Qiao. Modular Verification of SPARCv8 Code
  • Ulrich Schöpp. Particle-Style Geometry of Interaction as a Module System
  • Hideyuki Kawabata, Yuta Tanaka, Mai Kimura and Tetsuo Hironaka. Traf: a Graphical Proof Tree Viewer Cooperating with Coq through Proof General
  • James Brotherston and Max Kanovich. On the Complexity of Pointer Arithmetic in Separation Logic
  • Fabian Kunze, Gert Smolka and Yannick Forster. Formal Verification of a Call-by-value Lambda Calculus Machine
  • Shingo Eguchi, Naoki Kobayashi and Takeshi Tsukada. Automated Synthesis of Functional Programs with Auxiliary Functions
  • Xuan Bach Le, Aquinas Hobor and Anthony Widjaja Lin. Complexity Analysis of Tree Share Structure
  • Thibault Suzanne and Antoine Miné. Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Model
  • Beniamino Accattoli and Giulio Guerrieri. Types of Fireballs
  • Quang Loc Le and Mengda He. A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints
  • Daniel Hillerström and Sam Lindley. Shallow Effect Handlers
  • Timothy Jones and Michael Homer. The Practice of a Compositional Functional Programming Language
  • Andreea Costea, Wei-Ngan Chin, Shengchao Qin and Florin Craciun. Automated Modular Verification for Relaxed Communication Protocols