AndrasKovacs/sysF-NbE

Stars
1
Language Agda
License
MIT License
Created almost 8 years ago
Updated almost 8 years ago

AndrasKovacs/sysF-NbE

AndrasKovacs

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

Normalization by evaluation for intrinsic System F

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

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.

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.

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.