GitHub topics: normalization-by-evaluation
brendanzab/language-garden
A garden of small programming language implementations 🪴
Language: OCaml - Size: 2.22 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 282 - Forks: 6
TOTBWF/teenytt
A Teeny Type Theory
Language: Haskell - Size: 199 KB - Last synced at: 1 day ago - Pushed at: over 3 years ago - Stars: 27 - Forks: 3
RedPRL/algaett
🦠An experimental elaborator for dependent type theory using effects and handlers
Language: OCaml - Size: 620 KB - Last synced at: about 2 months ago - Pushed at: almost 2 years ago - Stars: 37 - 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: 9 months ago - Pushed at: over 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: over 1 year ago - Pushed at: over 3 years ago - Stars: 90 - Forks: 7
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: 9 months ago - Pushed at: over 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: over 2 years ago - Pushed at: over 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: 9 months ago - Pushed at: about 7 years ago - Stars: 0 - Forks: 0