Pinned Repositories
cctt
high-performance cubical evaluation
dtt-rtcg
Demo for dependent types + runtime code generation
elaboration-zoo
Minimal implementations for dependent type checking and elaboration
flatparse
Fast parsing from bytestrings
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/staged
Staged compilation with dependent types
AndrasKovacs/flatparse
Fast parsing from bytestrings
AndrasKovacs/cctt
high-performance cubical evaluation
AndrasKovacs/dtt-rtcg
Demo for dependent types + runtime code generation
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/antifunext
antifunext
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/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/gc-benchmarks
garbage collection benchmarks
AndrasKovacs/primdata
AndrasKovacs/AndrasKovacs.github.io
My github page
AndrasKovacs/aeson
A fast Haskell JSON library
AndrasKovacs/ghc-strict-implicit-params
GHC plugin for making implicit parameters strict
AndrasKovacs/parsnip
AndrasKovacs/souffle-haskell
Haskell bindings for the Souffle datalog language
AndrasKovacs/StepULC
Efficient and single-steppable ULC evaluation algorithm
AndrasKovacs/TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
AndrasKovacs/www
Webpages of course Programming Language Technology