smalltt

Tech stack & purpose

Smalltt is a demo project for high-performance elaboration techniques in dependent type theory, written in Haskell. The project showcases several design approaches including normalization-by-evaluation, contextual metavariables, glued evaluation, and approximate conversion checking, with the goal of demonstrating techniques that can scale to feature-complete languages while maintaining excellent performance. The implementation includes benchmarking code designed to be comparable across Agda, Lean, Coq, Idris 2, and smalltt itself, and the project's author is András Kovács, who also created the elaboration-zoo educational resource.

Community & reference links

• davidchristiansen.dk/tutorials/nbe/
• github.com/AndrasKovacs/elaboration-zoo
• this
• this file
• normalization benchmarks
• old smalltt version
• Coquand's algorithm

Languages

Contributors

• 
  András Kovács111 commits · 549 followers
• 
  András Kovács76 commits · 549 followers
• 
  András Kovács6 commits · 549 followers
• 
  Vladislav Zavialov1 commits · 234 followers
• 
  Sebastian Ullrich1 commits · 348 followers