Seminar details
Abstract:
We argue for a programming model where automated reasoning plays a key
role during (1) interactive program development, (2) program
compilation, and (3) program execution. I will focus on data
manipulation (as opposed to control). I outline our recent results in
complete functional synthesis for integer arithmetic, which is a form
of program compilation based on decision procedures. For program
development, I outline our ongoing work on resolution theorem proving
for interactive synthesis. For program execution, I touch upon the
UDITA system based on Java Pathfinder, and argue that programming
models related to constraint logic programming should play a bigger
role in mainstream software.
For more information, please see: http://lara.epfl.ch/w/impro
