TypeSig Talks: Program Synthesis by Semantics

TypeSig talks are back, and we’ve got a banger for you!

Zoey Shepherd, a PhD student at the University of Edinburgh School of Informatics is coming in to give a talk on program synthesis.

Details

Date: Monday, 9th of November, 2026
Location: Appleton Tower Lecture Theatre 4, University of Edinburgh
Time: 17:00-18:30

As always, free pizza will be provided!

Sign up

Sign up here! Spaces are limited, so sign up fast!

Talk Info

Title: Program Synthesis by Semantics

Abstract:

Program synthesis is, funnily enough, the work of synthesising programs. We start with some formal specification, and use methods from domains like logic and verification to build a program that meets the spec. This differs from vibe coding, firstly in that we avoid giving Anthropic any money, but also in that we get a guarantee of correctness by construction: we build our synthesis algorithm such that if it produces a program, then that program must meet the specification.

One would expect that synthesising a program, that is a term in a language, would involve looking carefully at the structure of that language, its semantics and type theories, and using that insight to inform the synthesis procedure. In truth, though, most synthesis work is agnostic to its target language. Syntax is a context-free grammar of opaque symbols; types are non-terminal symbols so that $t & t$ is a Boolean and $t + t$ is a number; and the semantics, if one exists, is a collection of Horn clauses.

It’s my opinion that the field of program synthesis could benefit from better connections with the rest of programming language theory, and my work is in trying to build those connections. I’ll be presenting NSynC, for Normalised Synthesis of Computation (there was some discussion about what the C was going to stand for), which is our early exploration of this building on type-directed synthesis work by Osera and Zdancewic. In NSynC, we synthesise terms by first searching for a semantics that satisfies the specification and then reifying that into a normal form, allowing us to completely quotient our search space by the language’s equational theory. This mirrors the reflect/reify procedure used in normalisation by evaluation, which we borrow concepts from heavily.