JetBrains Research unites scientists working in challenging new disciplines

Seminar on Lazy Functional Synthesis from First-Order Specifications

In this talk, we'll consider a recently presented technique for generating a non-recursive function implementation from a declarative specification formulated as a ∀∃-formula in first-order logic. The technique is based on lazy quantifier elimination via iterative computation of model-based projections of the specification and allows to synthesize functions with multiple outputs.

Supplementary materials:

http://www.cs.princeton.edu/~grigoryf/aeval.pdfhttp://sat.inesc-id.pt/~mikolas/lpar15.pdfPresenter: Dmitry Mordvinov

Date: February 25, 2019

Time: 17:15

Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28