András Kovács

elaboration-zoo. Minimal implementations for dependent type checking and elaboration

smalltt. Demo for high-performance type theory elaboration

staged. Staged compilation with dependent types

flatparse. Fast parsing from bytestrings

cctt. high-performance cubical evaluation

dtt-rtcg. Demo for dependent types + runtime code generation

setoidtt. Prototype implementations of systems based on setoid type theory

system-f-omega. System F-omega normalization by hereditary substitution in Agda

staged-fusion. Staged push/pull fusion with typed Template Haskell

normalization-bench. Lambda normalization and conversion checking benchmarks for various implementations

implicit-fun-elaboration. Implementation for ICFP 2020 paper

antifunext. antifunext

sett. Setoid type theory implementation

2ltt-impl. Eventually a practical 2-level TT-based compiler

universes. Generalized syntax & semantics for universe hierarchies

polynomial-model. A polynomial model of a Martin-Löf type theory + a bit of game semantics

thesis. my phd thesis

stlc-nbe. Correctness of normalization-by-evaluation for STLC

misc-stuff. Code for tutorials, papers and experiments. Mostly Agda, Coq and Haskell.

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

SemanticsWithApplications. Formal semantics in Agda.

preordertt. Experiments with preordered set models of (directed) type theories

pny1-assignment. College assignment writing in which I ramble about type classes and dependent types.

qiit-generalizations. Extending small finitary QIITs to non-small non-finitary

array-primops. Extra foreign primops for primitive arrays.

singleton-nats. Unary natural numbers relying on the singletons infrastructure

dawg. Generation and traversal of highly compressed directed acyclic word graphs.

trie-vector. Clojure-style persistent vector for Haskell.

BasicHs. Basic Haskell ("funkcionális programozás gyakorlat") lecture notes

HaladoHs. 2018 Spring "Haladó Haskell" ("Advanced Haskell") course materials (in Hungarian)

dynamic-array. Haskell

dynamic-mvector. A wrapper around MVector that enables push/pop/append functionality.

dawg-gen. Creates highly compressed directed acyclic word graphs from word lists.

primdata. Haskell

gc-benchmarks. garbage collection benchmarks

ind-ind-types. Materials for TYPES 2019 submissions about inductive-inductive types

func-lang-2019-1. Funkcionális nyelvek (IPM-18sztKVFPNYEG), 2019 tavasz, EA + GY

glue. Glued models of type theory, using internal languages

vector-hashtables. Haskell

bi-zipper. Simple bidirectional zipper from any Traversable.

shopping-list. Minimal shopping list app as college course assignment , in JS

scrabble-bot. Scrabble move generation