PV2 ⊧ SynPlexitysynthesises recursive functions that satisfy a functional specification and an asymptotic resource bound

Synthesis tool for recursive functions that satisfy both a functional specification and an asymptotic resource bound. Example usage: User asks the tool to synthesize an implementation of a sorting function with resource usage O(n log n) where n is the length of the input list.

Application domain/field

• Program synthesis
• Resource bound
• Recursive functions
• Resource-bound analysis

Type of tool

Synthesis tool

Expected input

• Refinement type that describes both the functionality and the asymptotic (big-O) resource usage of a program
• Set of auxiliary functions that the synthesized program can use

Format:

.sq file?

Internals

Implemented on top of Synquid, uses Z3. It uses a type-directed synthesis algorithm.

Comments

License: MIT license