Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.

@article{paperbot2153,
  title = {A correct-by-construction conversion from lambda calculus to combinatory logic},
  author = {WOUTER SWIERSTRA},
  journal = {Journal of Functional Programming},
  volume = {33},
  year = {2023},
  doi = {10.1017/s0956796823000084}
}