9 open source projects by AndrasKovacs

Demo for high-performance type theory elaboration

Minimal implementations for dependent type checking and elaboration

Staged compilation with dependent types

Lambda normalization and conversion checking benchmarks for various implementations

Implementation for ICFP 2020 paper

Rust-style strict Maybe in Haskell: no space/indirection overhead.

Prototype implementations of systems based on setoid type theory

Fast parsing from bytestrings

System F-omega normalization by hereditary substitution in Agda