LARA

Lecture 10: Quantifier Elimination, Partial Evaluation, and Synthesis

From Constraint Solving to Synthesis

Quantifier Elimination Basics

Quantifier Elimination Definition

QE from Conjunction of Literals Suffices

Definition of Presburger Arithmetic

QE for Presburger Arithmetic

Synthesis

Comfusy tool demo

William Cook: Online Partial Evaluation of Model Interpreters

Talk Video

A reference on partial evaluation: Partial Evaluation and Automatic Program Generation

A partial evaluation system: TEMPO