The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Functional correctness for non-trivial properties of software requires inductive proof. Sadly this is an undecidable problem which typically requires frustrating amounts of user guidance. Fortunately, this makes it a fascinating topic for research; indeed, a significant strand of research considers heuristic approaches to inductive theorem proving, driven by syntactic observations. Recently, a type-theory based form of synthesis, combined with an upside-down twist on rewriting, has led to some exciting results. In this talk I will outline the state the field, give my view of the key intuitions for the emerging proof strategies, and highlight the exciting challenges currently being considered.