hirrolot

arcgentica. An ARC-AGI solution using Agentica from Symbolica

macro_sequence_for. C

interaction-net-resources. :books: Interaction net resources

cubicaltt. Experimental implementation of Cubical Type Theory

spec_experiments. Some partial evaluation experiments

roguetype. The first ever roguelike written in the OCaml type system

opam. opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

minihm. toy implementation of Hindley-Milner type system that prints out inference steps

implicit-fun-elaboration. Implementation for ICFP 2020 paper

clap. Audio Plugin API

checked_oint. An OCaml library for checked integer arithmetic

NbE. Idris

system-f-omega-agda. A formalization of System Fω in Agda

Aptwe. A well typed by construction kernel language for bidirectional programming

hirrolot.github.io. My personal blog

anti-unification. Functional implementation of anti-unification algorithm for multiple terms

anyhow. Flexible concrete Error type built on std::error::Error

semver. Semantic Versioning Specification

git-filter-repo. Quickly rewrite git repository history (filter-branch replacement)

blurelf. Smoothen your executables

clay. High performance UI layout library in C.

DCC. Implementation of Defunctionalized Calculus of Constructions (Master thesis)

agda-simple-scp. A simple supercompiler formally verified in Agda

malfunction. Malfunctional Programming

hosc. Higher-Order Supercompiler

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

opam-repository. Main public package repository for opam, the source package manager of OCaml.

Higher-Order-Supercompiler. An implementation of the higher-order supercompilation algorithm as described in the paper "On the Termination of Higher-Order Positive Supercompilation"

Higher-Order-Deforester. Implementation of Higher Order Deforestation as described in the paper "Higher Order Deforestation"

ppx_blob. OCaml ppx to include binary data from a file as a string

ad-astra. Scripting language for Rust.

ScalarEvolution. An obscure Minecraft mod about computer technology and electronics based on RVVM project

ollvm. An higher-level LLVM binding for OCaml

ocaml-hashcons. OCaml hash-consing library

boehm-rs. Rust interface to BoehmGC providing global allocator implementation that uses this GC

hyperfine. A command-line benchmarking tool

domainslib. Parallel Programming over Domains

teloxide_tests. A library that adds the ability to test teloxide bots by bot mocking!

delimcc. Delimited continuations in byte-code and native OCaml

PPMP-Iceberg. Preprocessor metaprogramming knowledge obscurity chart

wttr.in. :partly_sunny: The right way to check the weather

lady-deirdre. Compiler front-end foundation technology.

teloxide. 🤖 An elegant Telegram bots framework for Rust

dptree. Asynchronous event dispatch for Rust

teloc. Simple, compile-time DI framework for Rust

mazeppa. A modern supercompiler for call-by-value functional languages

guarded-absint. Guarded abstract interpretation

Brainfuck. A Brainfuck interpreter written in Agda

8cc.vim. C Compiler written in Vim script

BOHM1.1. Bologna Optimal Higher-Order Machine, Version 1.1

CP-next. The Next Generation of Compositional Programming

staged. Staged compilation with dependent types

mirage. Mirage Persistent Kernel: Compiling LLMs into a MegaKernel

ChezScheme. Chez Scheme

Distiller. Implementation of the distillation algorithm as described in the paper "Distillation: Extracting the Essence of Programs".

Higher-Level-Transformer. Higher-Level Transformer as described in the paper "The Next 700 Program Transformers"

narya. A proof assistant for higher-dimensional type theory

reopt. A tool for analyzing x86-64 binaries.

ppx_variants_conv. Generation of accessor and iteration functions for ocaml variant types

int_repr. Integers of various widths

gcc-exceptions. C++

HVM2. A massively parallel, optimal functional runtime in Rust

holyc-lang. HolyC compiler & transpiler

mal. mal - Make a Lisp

interaction-calculus-of-constructions. A minimal proof checker.

Refal-05. Компилятор Рефала-5 в Си

mrefal. Компилятор Модульного Рефала

refal-5-lambda. Компилятор Рефала-5λ

meta-cedille. Minimalistic dependent type theory with syntactic metaprogramming

typefuck-haskell. Typelevel Brainfuck; Brainfuck implemented solely in Haskell's type system (no TemplateHaskell)

bap. Binary Analysis Platform

spsc. SPSC: A Small Positive Supercompiler

cayenne. Resurrecting Lennart Augustsson's implementation of Cayenne

c-vector. A dynamic array implementation in C similar to the one found in standard C++

sat-inv-matrix. Implementing integer matrix inversion with SAT solver

Arend. The Arend Proof Assistant

PPLISP. c-prepocessor lisp

lone. The standalone Linux Lisp

ttstar. Dependently typed core calculus with erasure

higher_kinded. A library with an encoding of higher kinded types in OCaml

semgrep. Lightweight static analysis for many languages. Find bug variants with patterns that look like source code.

awesome-ocaml. A curated collection of awesome OCaml tools, frameworks, libraries and articles.

clap. Command-Line Argument Parsing, imperative style with a consumption mechanism.

pprint. A pretty-printing combinator library for OCaml

snowden-archive. 💥 A collection of all documents leaked by former NSA contractor and whistleblower Edward Snowden.

menby. modular nbe!

serde-blocked. I have created this repository to check who has been muted for expressing support on https://github.com/serde-rs/serde/pull/2580

lambda-calculus-hs. A bestiary of lambda calculus

bdwgc. The Boehm-Demers-Weiser conservative C/C++ Garbage Collector (bdwgc, also known as bdw-gc, boehm-gc, libgc)

compilers-targeting-c. A list of compilers that can generate C code

lambdapi. Dependently Typed Lambda Calculus in Haskell

sc-mini. SC Mini is a "minimal" positive supercompiler

imaging. Imaging is a simple image processing package for Go

gg. Go Graphics - 2D rendering in Go with a simple API.

ocaml-h2. An HTTP/2 implementation written in pure OCaml

minilisp. A readable lisp in less than 1k lines of C

spartan-type-theory. Spartan type theory

idris-jvm. Idris on the JVM

type-systems. Implementations of various type systems in OCaml.

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

odep. Dependency graphs for OCaml modules, libraries and packages

dream. Tidy, feature-complete Web framework

ppx_string_interpolation. PPX rewriter that enables string interpolation in OCaml

ocaml-spectrum. Library for color and formatting in the terminal

cauldron. A collection of single-file C libraries. (generic containers, random number generation, argument parsing and other functionalities)

clib. Header-only library for C99 that implements the most important classes from GLib: GArray, GHashTable, GList and GString.

eio. Effects-based direct-style IO for multicore OCaml

trapcc. Computing with traps

language-garden. A garden of small programming language implementations 🪴

ocamlformat. Auto-formatter for OCaml code

RVVM. The RISC-V Virtual Machine

instaparse. Clojure

d2-docs. Language documentation and blog for D2.

jsoncrack.com. ✨ Innovative and open-source visualization application that transforms various data formats, such as JSON, YAML, XML and CSV into interactive graphs.

d3. Bring data to life with SVG, Canvas and HTML. :bar_chart::chart_with_upwards_trend::tada:

datatt. A dependent type theory with user defined data types

notty. Declarative terminal graphics for OCaml

lambda-term. Terminal manipulation library for OCaml

ocaml-caqti. Cooperative-threaded access to relational data

pp_loc. Pretty-printing for error source locations

saturn. Lock-free data structures for multicore OCaml

monadic. A monad transformers library for OCaml, based on transformers and mtl

preface. Preface is an opinionated library designed to facilitate the handling of recurring functional programming idioms in OCaml.

oxcaml. OCaml - Oxidized!

ppx_fields_conv. Generation of accessor and iteration functions for ocaml records

ocaml. The core OCaml system: compilers, runtime system, base libraries

comby. A code rewrite tool for structural search and replace that supports ~every language.

opium. Sinatra like web toolkit for OCaml

eliom. Multi-tier framework for programming web and mobile applications in OCaml.

magic-trace. magic-trace collects and displays high-resolution traces of what a process is doing

type-systems. Playing with type systems

ppx_let. Monadic let-bindings

mina. Mina is a cryptocurrency protocol with a constant size blockchain, improving scaling while maintaining decentralization and security.

irmin. Irmin is a distributed database that follows the same design principles as Git

ounit. OCaml

bisect_ppx. Code coverage for OCaml and ReScript

alcotest. A lightweight and colourful test framework

ounit-simple-test. A (borrowed) example of unit testing OCaml code with OUnit. A reminder for myself.

cmdliner. Declarative definition of command line interfaces for OCaml

ppx_deriving. Type-driven code generation for OCaml

dune. A composable build system for OCaml.

ocaml-containers. A lightweight, modular standard library extension, string library, and interfaces to various libraries (unix, threads, etc.) BSD license.

core. Jane Street Capital's standard library overlay

coz. Coz: Causal Profiling

normalization-by-evaluation. Various implementations of normalization by evaluation.

smalltt. Demo for high-performance type theory elaboration

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

pygments. Pygments is a generic syntax highlighter written in Python

fp. A small, weird and unpractical programming language.

giscus. A commenting system powered by GitHub Discussions. :octocat: :speech_balloon: :gem:

lambda-8cc. x86 C compiler written in untyped lambda calculus

cvec. No bullshit vector library for C

learn-idris-pub. Public data for https://learn-idris.net/

pldb. PLDB: a Programming Language DataBase

enso. Enso Analytics is a self-service data prep and analysis platform designed for data teams.

lean4. Lean 4 programming language and theorem prover

lean3. Lean Theorem Prover

usql. Universal command-line interface for SQL databases

tinn. A tiny neural network library

ExtractTable-py. Python library to extract tabular data from images and scanned PDFs

go-app. A package to build progressive web apps with Go programming language and WebAssembly.

go. The Go programming language

anvil-runtime. The runtime engine for hosting Anvil web apps

activate-linux. The "Activate Windows" watermark ported to Linux

nursery. Structured Concurrency in Go

ikos. Static analyzer for C/C++ based on the theory of Abstract Interpretation.

nappgui. Cross-Platform C SDK (precompiled)

nappgui_src. SDK for building cross-platform desktop apps in ANSI-C

smolrtsp. A lightweight real-time streaming library for IP cameras

Yaffle. A core language and API for dependently typed languages

h264bitstream. A complete set of functions to read and write H.264 video bitstreams, in particular to examine or modify headers.

mass. A compiler for a new language focusing on compile-time execution and no LLVM dependency.

greatest. A C testing library in 1 file. No dependencies, no dynamic allocation. ISC licensed.

asmjit. Low-latency machine code generation

gray-matter. A colour scheme for Sublime Text and Visual Studio Code that takes design cues from popular minimalist Markdown text editors.

extensible-records. Extensible records for Idris

idris2-tls. A portable idris2 implementation of TLS

sirdi. Package manager for Idris

datatype99. Algebraic data types for C99

orca. C Multi-REST API library for Discord, Slack, Reddit, etc.

firmware. Alternative IP Camera firmware from an open community

ipctool. Simple tool (and library) for checking IP camera hardware

terra. Terra is a low-level system programming language that is embedded in and meta-programmed by the Lua programming language.

idris2-async. Small async library for idris2, inspired by purescript-aff

args. An argument-parsing library for C.

scala-nodejs-python-example. Example which demonstrates calling NodeJS and Python functions from Scala.

gf. A GDB frontend for Lïnux.

fdk-aac. A standalone library of the Fraunhofer FDK AAC code from Android.

hello-world.rs. 🚀Memory safe, blazing fast, configurable, minimal hello world written in rust(🚀) in a few lines of code with few(1247🚀) dependencies🚀

category-theory-resources. Resources for learning Category Theory for an enthusiast

slangify. Let's get mad lads!!!

funlangs. Functional languages index

katla. Idris

idris-qsort. Verified Quicksort in Idris 2

TermGL. 2D & 3D graphics engine in the terminal [C/C++]

cisp. A C preprocessor library implementing object semantics.

binom. C macro that computes binominal coefficient at compile time

flix. The Flix Programming Language

argtable3. A single-file, ANSI C, command-line parsing library that parses GNU-style command-line options.

libass. libass is a portable subtitle renderer for the ASS/SSA (Advanced Substation Alpha/Substation Alpha) subtitle format.