APLAS 2020
Mon 30 November - Wed 2 December 2020
Mon 30 Nov 2020 18:00 - 18:30 at online - Types Chair(s): Marco Servetto

Kobayashi et al.\ have recently shown that various verification problems for higher-order functional programs can naturally be reduced to the validity checking problem for $\text{HFL}\mathbb{Z}$, a higher-order fixpoint logic extended with integers. We propose a refinement type system for checking the validity of $\nu\text{HFL}\mathbb{Z}$ formulas, where $\nu\text{HFL}\mathbb{Z}$ is a fragment of $\text{HFL}\mathbb{Z}$ without least fixpoint operators, but sufficiently expressive for encoding safety property verification problems. Our type system has been inspired by the type system of Burn et al. for solving the satisfiability problem for HoCHC, which is essentially equivalent to the $\nu\text{HFL}\mathbb{Z}$ validity checking problem. Our type system is more expressive, however, due to a more sophisticated subtyping relation. We have implemented a type-based $\nu\text{HFL}\mathbb{Z}$ validity checker ${\rm R{\small e}THFL}$ based on the proposed type system, and confirmed through experiments that ${\rm R{\small e}THFL}$ can solve more instances than Horus, the tool based on Burn et al.’s type system.

#### Mon 30 NovDisplayed time zone: Osaka, Sapporo, Tokyo change

 17:30 - 19:30 TypesResearch Papers at online Chair(s): Marco Servetto Victoria University Wellington, New Zealand 17:3030mTalk Syntactically Restricting Bounded Polymorphism for Decidable SubtypingResearch PapersJulian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington 18:0030mTalk A New Refinement Type System for Automated nu-HFLZ Validity CheckingResearch PapersHiroyuki Katsura The University of Tokyo, Naoki Iwayama University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan 18:3030mTalk Behavioural Types for Memory and Method Safety in a Core Object-Oriented LanguageResearch PapersMario Bravetti Università di Bologna, Adrian Francalanza University of Malta, Iaroslav Golovanov Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mathias Steen Jakobsen Department of Computer Science, Aalborg University, Denmark, Mikkel Klinke Kettunen Department of Computer Science, Aalborg University, Denmark, Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS 19:0030mTalk Neural Networks, Secure by Construction: An Exploration of Refinement TypesResearch PapersWen Kokke University of Edinburgh, Ekaterina Komendantskaya Heriot-Watt University, UK, Daniel Kienitz Heriot-Watt University, David Aspinall University of Edinburgh, Robert Atkey University of Strathclyde