GitHub topics: normalization-by-evaluation
RedPRL/algaett
🦠An experimental elaborator for dependent type theory using effects and handlers
Language: OCaml - Size: 620 KB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 35 - Forks: 0
fsestini/nbe-mltt-wes
Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.
Language: Agda - Size: 26.4 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0
brendanzab/rust-nbe-for-mltt
Normalization by evaluation for Martin-Löf Type Theory with dependent records
Language: Rust - Size: 862 KB - Last synced at: 11 months ago - Pushed at: almost 3 years ago - Stars: 90 - Forks: 7
TOTBWF/teenytt
A Teeny Type Theory
Language: Haskell - Size: 199 KB - Last synced at: 7 days ago - Pushed at: almost 3 years ago - Stars: 26 - Forks: 3
fsestini/nbe-weak-stlc
Agda formalization of normalization by evaluation for the confluent simply-typed weak lambda-calculus.
Language: Agda - Size: 29.3 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 8 - Forks: 0
nguermond/normalization-by-evaluation
Various implementations of normalization by evaluation.
Language: OCaml - Size: 63.5 KB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 2 - 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