Reconciling reliability and flexibility with progressive typing

“Typed” programming languages carry out checks prior to their execution, but are often abandoned in favour of “untyped” languages, which are simpler but less reliable. Polyvalent, progressive typing allows these checks to be limited to certain parts of the program. A mathematical interpretation of this technique will make it possible to use it more precisely and efficiently.