ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 12:00 - 12:30 at SUN II - Program Verification Chair(s): Luís Caires

Incremental computation has recently been studied using the concepts of change structures and derivatives of programs, where the derivative of a function allows updating the output of the function based on a change to its input. We generalise change structures to change actions, and study their algebraic properties. We develop change actions for common structures in computer science, including directed-complete partial orders and Boolean algebras. We then show how to compute derivatives of fixpoints. This allows us to perform incremental evaluation and maintenance of recursively defined functions with particular application generalised Datalog programs. Moreover, unlike previous results, our techniques are modular in that they are easy to apply both to variants of Datalog and to other programming languages.

Mon 8 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Program VerificationESOP at SUN II
Chair(s): Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
10:30
30m
Talk
Time Credits and Time Receipts in Iris
ESOP
Glen Mével, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, François PottierInria, France
Link to publication
11:00
30m
Talk
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
ESOP
Guido MartínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor DumitrescuNomadic Labs Paris, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal NarasimhamurthyUniversity of Colorado, Boulder, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication
11:30
30m
Talk
Semi-Automated Reasoning About Non-Determinism in C Expressions
ESOP
Dan FruminRadboud University, Léon GondelmanLRI, Université Paris-Sud, Robbert KrebbersDelft University of Technology
Link to publication
12:00
30m
Talk
Fixing Incremental Computation: Derivatives of fixpoints, and the recursive semantics of Datalog
ESOP
Michael Peyton JonesIOHK, Mario Alvarez-PicalloUniversity of Oxford, Alexander Eyers-TaylorSemmle, C.-H. Luke OngUniversity of Oxford
Link to publication