AndrasKovacs/misc-stuff

Stars
19
Rank 1,163,249 (Top 23 %)
Language Agda
License
MIT License
Created almost 9 years ago
Updated almost 2 years ago

AndrasKovacs/misc-stuff

AndrasKovacs

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

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

elaboration-zoo

Minimal implementations for dependent type checking and elaboration

smalltt

Demo for high-performance type theory elaboration

flatparse

Fast parsing from bytestrings

staged

Staged compilation with dependent types

cctt

high-performance cubical evaluation

setoidtt

Prototype implementations of systems based on setoid type theory

staged-fusion

Staged push/pull fusion with typed Template Haskell

system-f-omega

System F-omega normalization by hereditary substitution in Agda

normalization-bench

Lambda normalization and conversion checking benchmarks for various implementations

implicit-fun-elaboration

Implementation for ICFP 2020 paper

sett

Setoid type theory implementation

polynomial-model

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

universes

Generalized syntax & semantics for universe hierarchies

thesis

stlc-nbe

Correctness of normalization-by-evaluation for STLC

flat-maybe

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

preordertt

Experiments with preordered set models of (directed) type theories

SemanticsWithApplications

Formal semantics in Agda.

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

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)

array-primops

Extra foreign primops for primitive arrays.

ind-ind-types

Materials for TYPES 2019 submissions about inductive-inductive types

dynamic-array

primdata

dynamic-mvector

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

antifunext

AndrasKovacs.github.io

func-lang-2019-1

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

dawg-gen

Creates highly compressed directed acyclic word graphs from word lists.

elements-of-compsys

Projects for the book "The Elements of Computing Systems"

glue

Glued models of type theory, using internal languages

scrabble-bot

Scrabble move generation

bi-zipper

Simple bidirectional zipper from any Traversable.

elte-cbsd

"Component based software development" course assignments.

sysF-NbE

Normalization by evaluation for intrinsic System F

haskell-performance

Miscellaneous Haskell benchmarks

gc-benchmarks

garbage collection benchmarks

bf

Fast Haskell brainfuck interpreter

while-hs

Translation of an undergrad course compiler to Haskell.