@article{partialcalc,
  author = {Bahr, Patrick},
  title = {Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations},
  year = {2026},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {10},
  number = {ICFP},
  url = {https://doi.org/10.1145/3828683},
  doi = {10.1145/3828683},
  abstract = {Compiler calculation is a technique for deriving a
  correct-by-construction compiler from the specification of the
  compiler's correctness. In this setting, the compiler specification
  typically states that the semantics of each compiled program is
  \emph{bisimilar} to the semantics of the original source program,
  i.e.\ both programs have the same behaviour. However, full
  bisimilarity for all source programs is too strong a requirement for
  complex source languages with unsafe behaviour for which the
  compiler need not make any guarantees, e.g.\ because programs that
  exhibit unsafe behaviour are ruled out by the type checker. This has
  long been recognised and exploited in compiler verification, but to
  date no calculation technique can handle such partial
  specifications. To address this, we propose a generalisation of
  bisimilarity, called \emph{skew bisimilarity}, that allows us to
  weaken the compiler specification so that we may safely ignore
  unsafe behaviour when calculating a compiler for the specification.
  We demonstrate that skew bisimilarity enables us to derive compilers
  that produce more efficient code compared to previous compiler
  calculation techniques, all while maintaining the same strong
  correctness guarantees for safe source programs.

  We further show that -- even for source languages without unsafe behaviour
  -- skew bisimilarity provides a powerful generalisation of
  bisimilarity that enables a novel calculation technique for
  reasoning about \emph{register machines}. This improves on existing
  compiler calculation techniques for register machines, which are
  currently limited to terminating source languages without effects.
  To demonstrate the effectiveness of skew bisimilarity as a proof
  technique for compiler calculation, we have fully formalised it in
  Agda and used this formalisation to calculate compilers for a
  variety of languages, including the first calculation of a compiler
  for a typed concurrent lambda calculus that targets a register
  machine.},
  journal = {Proceedings of the ACM on Programming Languages},
  month = aug,
  articleno = {285},
  numpages = {34},
  keywords = {bisimilarity, choice trees, program calculation, register machine}
}