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

Subtyping of Bounded Polymorphism has long been known to be undecidable when coupled with contra-variance. While decidable forms of bounded polymorphism exist, they all either sacrifice useful properties such as contra-variance (Kernel F${<:}$), or useful metatheoretic properties (F${<:}^\top$). In this paper we show how by syntactically separating contra-variance from the recursive aspects of subtyping in System F${<:}$, decidable subtyping can be ensured while also allowing for both contra-variant subtyping of certain quantified types, and many of System F${<:}$’s desirable metatheoretic properties. We then show that this approach can be applied to the related polymorphism present in D$_{<:}$, a minimal calculus that models core features of the Scala type system.

Mon 30 Nov
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

17:30 - 19:30: TypesResearch Papers at online
Chair(s): Marco ServettoVictoria University Wellington, New Zealand
17:30 - 18:00
Talk
Syntactically Restricting Bounded Polymorphism for Decidable Subtyping
Research Papers
Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington
18:00 - 18:30
Talk
A New Refinement Type System for Automated nu-HFLZ Validity Checking
Research Papers
Hiroyuki KatsuraThe University of Tokyo, Naoki IwayamaUniversity of Tokyo, Japan, Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaChiba University, Japan
18:30 - 19:00
Talk
Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language
Research Papers
Mario BravettiUniversità di Bologna, Adrian FrancalanzaUniversity of Malta, Iaroslav GolovanovDepartment of Computer Science, Aalborg University, Hans HüttelDepartment of Computer Science, Aalborg University, Mathias Steen JakobsenDepartment of Computer Science, Aalborg University, Denmark, Mikkel Klinke KettunenDepartment of Computer Science, Aalborg University, Denmark, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS
19:00 - 19:30
Talk
Neural Networks, Secure by Construction: An Exploration of Refinement Types
Research Papers
Wen KokkeUniversity of Edinburgh, Ekaterina KomendantskayaHeriot-Watt University, UK, Daniel KienitzHeriot-Watt University, David AspinallUniversity of Edinburgh, Robert AtkeyUniversity of Strathclyde