Gergő Érdi

metafun. Compile Haskell-like code into C++ template metaprograms

clash-spaceinvaders. Intel 8080-based Space Invaders arcade machine implemented on an FPGA, written in CLaSH

chirp8-avr. CHIP-8 implementation in Rust targeting AVR microcontrollers

tandoori. Compositional type checking for Haskell

clash-compucolor2. Clash implementation of the Compucolor II home computer

alef. Alef Lazily Evaluates Functions

icfp-bingo-2017-idris. ICFP Bingo 2017 (Idris edition)

clash-intel8080. Intel 8080 CPU core: software emulator and CLaSH hardware description

functional-mos6502-web-performance. https://unsafeperform.io/blog/2022-07-02-a_small_benchmark_for_functional_languages_targeting_web_browsers/

clashilator. Generate interface between Clash and Verilator

interaction-nets. Haskell implementation of interaction net-based lambda evaluation

mos6502-kansas-lava. Kansas Lava implementation of MOS 6502 microprocessor

stlc-agda. STLC-related snippets in Agda

universe-of-syntax. A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.

brainfuck-cpu-fpga. A CPU that uses Brainfuck as its machine code

chirp8-c64. Rust

syntactic-stlc. Syntactic evaluation of STLC (incl. proof of normalization a la Software Foundations)

generic-syntax. Library implementation of "Generic description of well-scoped, well-typed syntaxes"

clash-tinybasic. Tcl

retroclash-lib. Library code for upcoming RetroClash book

hm-compo. Compositional type checking for a Hindley-Milner type system

brainfuck64. Brainfuck compiler that runs on the Commodore 64 (or any 6502-based computer supported by cc65 that has enough RAM)

clash-pong. Pong in Haskell / Clash, running as software using SDL and as hardware targeting FPGAs

brainfuck. Brainfuck interpreter & compiler written in Haskell, with focus on readability instead of performance

brainfuck-cpu. Brainfuck CPU from simple logic gates

chip8-papilio. FPGA implementation of the Chip8 platform, in Kansas Lava

clash-shake. Haskell

scottcheck. Haskell

clash-flappysquare. Flappy Square, the Clash circuit from my Haskell Exchange 2022 talk

clash-sandbox. Playing around with CLaSH

mod-arith. Modular arithmetic in Agda

enigma-kansas-lava. Enigma machine implemented in Kansas Lava

free-applicative. Free applicative functors

chip8-haskell. CHIP-8 emulator

system-f-agda. System F

retroclash-book-code. Small example programs from the RetroClash book

chip8-clash. CHIP-8 implemented in CλaSH.

chirp8-engine. Rust

tinymicro-mos6502-kansas-lava. Tiny Microcomputer built around MOS6502 microprocessor

mgu-agda. Agda implementation of McBride's "First-order unification by structural recursion" paper

brainfuck-idris. Brainfuck interpreter in Idris

cubical-freemonoids. Free monoids take a price HIT

eightbit-kansas-lava. Kansas Lava implementation of eight-bit home computers

petbasic-parser. Idris

chirp8-avr-simulator. C++

clash-bounce-bench. Benchmark for various methods of simulating Clash

kansas-lava-papilio. Kansas Lava support files for the Papilio FPGA board

hindleymilner-agda. Hindley Milner type system modeled in Agda

chip-80. A CHIP-8 implementation for Z80

ratkai. Rátkai István szöveges kalandjátékaival kapcsolatos programok: Z80 verzió, és játékfejlesztési toolok

idris2-homelab. Idris

homelab2-games. Games for the HomeLab-2 home computer

hott-exercise. HoTT exercise for my Haskell.SG meetup talk on HoTT and CTT

codenames. Grid generator for Codenames & Codenames Duet

clash-calculator. FPGA desktop calculator for seven-segment display and keypad, written in Clash