Thu 11 Jan 2018 14:55 - 15:20 at Bunker Hill - Termination Chair(s): Constantin Enea

Formal frameworks for cost analysis of programs have been widely studied in the unary setting and, to a limited extent, in the relational setting. However, many of these frameworks focus only on the cost aspect, largely side-lining functional properties that are often a pre-requisite for cost analysis, thus leaving many interesting programs out of their purview. In this paper, we show that elegant, simple, expressive proof systems combining cost analysis and functional properties can be built by combining already known ingredients: higher-order refinements and cost monads. Specifically, we derive two syntax-directed proof systems, $R^C$ and $U^C$, for relational and unary cost analysis, by adding a cost monad to a (syntax-directed) logic of higher-order programs. We study the metatheory of the systems, show that several nontrivial examples can be verified in them, and prove that existing frameworks for cost analysis (RelCost and RAML) can be embedded in them.

Thu 11 Jan

13:40 - 15:20: Research Papers - Termination at Bunker Hill
Chair(s): Constantin EneaUniversité Paris Diderot
POPL-2018-papers151567440000013:40 - 14:05
Annabelle McIverMacquarie University, Carroll MorganUniversity of New South Wales; Data 61, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University
POPL-2018-papers151567590000014:05 - 14:30
Sheshansh AgrawalIIT Bombay, Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria
POPL-2018-papers151567740000014:30 - 14:55
Yangjia LiInstitute of Software, Chinese Academy of Sciences, Mingsheng YingUniversity of Technology Sydney
POPL-2018-papers151567890000014:55 - 15:20
Ivan RadicekTU Vienna, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Florian ZulegerTU Vienna