Generalized Church is the Curry-Howard of Knaster-Tarski

The proofs-as-programs principle (also known as the Curry-Howard isomorphism) sets up a correspondence between logical proof systems and type systems for programming languages. So occasionally a result is independently developed twice, once as a theorem and once as a program. Here’s a short and cute example of this phenomenon. (I read about it in this textbook, but I think it deserves to be better

[lotz84]

一般化されたチャーチエンコーディングはクナスタ・タルスキの定理と対応するのかー（白目）