A dependently-typed language with indexed inductive types supported.

A module for Blish-HUD that allows to customize the defeated screen.

A proof assistant and a dependently-typed language

A Typst-friendly static Zettelkästen site generator.

A case for representing data collections and objects in the LLVM IR

A type-driven and high-performance ORM framework in Rust

General-purposed C programming language API metadata registry

A Gradle plugin for streamlined publishing on Maven Central

Overrun Game Library is a high-performance library implemented with Java 25, enables cross-platform access to a set of C library bindings, and provides some useful utilities.

FlatLaf - Swing Look and Feel (with Darcula/IntelliJ themes support)

通用计算机图形学研究平台

Ghidra is a software reverse engineering (SRE) framework

AssetStudioMod - modified version of Perfare's AssetStudio, mainly focused on UI optimization and some functionality enhancements.

Implementation of CARVe in Beluga

The well-foundedness of the multiset ordering

我从动漫中学习到的知识和人生感悟

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Deprecated

Logical Relation for MLTT in Coq

antifunext

Code for a Necesse mod

A .DS_Store file disclosure exploit. It parses .DS_Store file and downloads files recursively.

Forge wonderful chat messages in typst

A toy dependent typed language.

Minimal example showing core dump in Lean4 with import of Mathlib.Control.Bifunctor

A language with dependent data and codata types

Amper - a build tool for the Kotlin and Java languages, with a focus on user experience and tooling