GitHub topics: system-t
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: 25 days ago - Pushed at: over 4 years ago - Stars: 12 - Forks: 0
cj-xu/GentzenTrans
A monadic translation of Gödel's System T in the spirit of Gentzen's negative translation
Language: Agda - Size: 49.8 KB - Last synced at: about 2 years ago - Pushed at: almost 5 years ago - Stars: 4 - Forks: 0
fsestini/nbe-weak-systemt
Normalization by Evaluation for a version of System T with combinatory weak conversion.
Language: Agda - Size: 52.7 KB - Last synced at: 5 months ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0
