@unpublished{sobycoty,
  author = {Patrick Bahr and Zac Garby and Graham Hutton},
  title = {Sound-By-Construction Type Systems},
  abstract = {Type systems for programming languages are usually designed by hand,
with the aim of satisfying a type soundness property that guarantees
well-typed programs cannot go wrong.  In this article, we show how
standard techniques for \emph{proving} type soundness can be used in
reverse to systematically \emph{derive} type systems
that are sound by construction.  We introduce and illustrate our
methodology with a series of practical examples, including a typed
lambda calculus with conditionals and checked exceptions.},
  Note = {Preprint, February 2026},
  Keywords = {program calculation, semantic types, type systems, logical relations},
  year = {2026},
  month = feb
}