Pinned Repositories
cctt
high-performance cubical evaluation
elaboration-zoo
Minimal implementations for dependent type checking and elaboration
flatparse
Fast parsing from bytestrings
implicit-fun-elaboration
Implementation for ICFP 2020 paper
normalization-bench
Lambda normalization and conversion checking benchmarks for various implementations
setoidtt
Prototype implementations of systems based on setoid type theory
smalltt
Demo for high-performance type theory elaboration
staged
Staged compilation with dependent types
staged-fusion
Staged push/pull fusion with typed Template Haskell
system-f-omega
System F-omega normalization by hereditary substitution in Agda
AndrasKovacs's Repositories
AndrasKovacs/elaboration-zoo
Minimal implementations for dependent type checking and elaboration
AndrasKovacs/smalltt
Demo for high-performance type theory elaboration
AndrasKovacs/flatparse
Fast parsing from bytestrings
AndrasKovacs/staged
Staged compilation with dependent types
AndrasKovacs/cctt
high-performance cubical evaluation
AndrasKovacs/staged-fusion
Staged push/pull fusion with typed Template Haskell
AndrasKovacs/normalization-bench
Lambda normalization and conversion checking benchmarks for various implementations
AndrasKovacs/implicit-fun-elaboration
Implementation for ICFP 2020 paper
AndrasKovacs/sett
Setoid type theory implementation
AndrasKovacs/polynomial-model
A polynomial model of a Martin-Löf type theory + a bit of game semantics
AndrasKovacs/universes
Generalized syntax & semantics for universe hierarchies
AndrasKovacs/thesis
my phd thesis
AndrasKovacs/misc-stuff
Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.
AndrasKovacs/flat-maybe
Rust-style strict Maybe in Haskell: no space/indirection overhead.
AndrasKovacs/pny1-assignment
College assignment writing in which I ramble about type classes and dependent types.
AndrasKovacs/qiit-generalizations
Extending small finitary QIITs to non-small non-finitary
AndrasKovacs/singleton-nats
Unary natural numbers relying on the singletons infrastructure
AndrasKovacs/dynamic-array
AndrasKovacs/dynamic-mvector
A wrapper around MVector that enables push/pop/append functionality.
AndrasKovacs/primdata
AndrasKovacs/AndrasKovacs.github.io
My github page
AndrasKovacs/aeson
A fast Haskell JSON library
AndrasKovacs/environment-bench
Benchmarking compiler representations of variable environments
AndrasKovacs/ghc-strict-implicit-params
GHC plugin for making implicit parameters strict
AndrasKovacs/ghc-whole-program-compiler-project
GHC Whole Program Compiler and External STG IR tooling
AndrasKovacs/lennart-lambda
λλλλ Lennart Augustsson's λ-calculus cooked four ways
AndrasKovacs/megaparsec
Industrial-strength monadic parser combinator library
AndrasKovacs/parsnip
AndrasKovacs/souffle-haskell
Haskell bindings for the Souffle datalog language
AndrasKovacs/StepULC
Efficient and single-steppable ULC evaluation algorithm