We describe preliminary work suggesting that most typing rules for a programming language can be obtained automatically from its operational semantics. Instead of going the usual way, to first define the semantics and the type system, and then show progress and preservation, we start from the semantics and construct a type system that satisfies progress and preservation by construction. We have tested our approach on simple lambda calculi and we have constructed a Haskell prototype that implements our algorithm.

• Two-page TYPES 2017 paper.


• TYPES 2017 presentation.


• Haskell implementation.


• The work is based on a Master thesis defended by Vlad Andrei Tudose in 2014.