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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30
Program VerificationESOP at SUN II
Chair(s): Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
10:30
30m
Talk
Time Credits and Time Receipts in Iris
ESOP
Glen Mével , Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, François Pottier Inria, France
Link to publication
11:00
30m
Talk
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
ESOP
Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu Nomadic Labs Paris, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy University of Colorado, Boulder, Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Link to publication
11:30
30m
Talk
Semi-Automated Reasoning About Non-Determinism in C Expressions
ESOP
Dan Frumin Radboud University, Léon Gondelman LRI, Université Paris-Sud, Robbert Krebbers Delft 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 Jones IOHK, Mario Alvarez-Picallo University of Oxford, Alexander Eyers-Taylor Semmle, C.-H. Luke Ong University of Oxford
Link to publication