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

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
TerminationResearch Papers at Bunker Hill
Chair(s): Constantin Enea Université Paris Diderot
13:40
25m
Talk
A new proof rule for almost-sure termination
Research Papers
Annabelle McIver Macquarie University, Carroll Morgan University of New South Wales; Data 61, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University
14:05
25m
Talk
Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Research Papers
Sheshansh Agrawal IIT Bombay, Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria
14:30
25m
Talk
Algorithmic Analysis of Termination Problems for Quantum Programs
Research Papers
Yangjia Li Institute of Software, Chinese Academy of Sciences, Mingsheng Ying University of Technology Sydney
14:55
25m
Talk
Monadic refinements for relational cost analysis
Research Papers
Ivan Radicek TU Vienna, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Florian Zuleger TU Vienna