jonsterling/agda-effectful-forcing

Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

Language: Agda - Size: 1.24 MB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 12 - Forks: 0