Lists (32)
📽 Animation
5 repositories
🖼️ Art
3 repositories
📜 Binary Formats
54 repositories
🌀 Bootstrapping
49 repositories
🏗️ Build systems
13 repositories
📝 Compilation
34 repositories
🎨 Creative Tools
38 repositories
🗄 Data Layout
3 repositories
🌱 Digital Gardens - Examples
10 repositories
🌱 Digital Gardens - Tools
42 repositories
📖 Documentation - Tools
3 repositories
🚀 Effects
Effect systems, Algebraic effects and handlers… resources, languages, libraries and use cases58 repositories
🗣 Elaboration
Examples of elaborating surface languages into minimal core languages26 repositories
🐟 Fish Shell
4 repositories
🔠 Fonts
28 repositories
🕹️ Game Development
4 repositories
🕹️ Games
2 repositories
📐 Geometric Algebra
18 repositories
👍 Memory Safe by Default
4 repositories
🍱 Module Systems - Case Studies
3 repositories
🍱 Module Systems - Languages
12 repositories
🏡 My Stack
14 repositories
⚙️ Nix - Example Configurations
12 repositories
⚙️ Nix - Tools
37 repositories
💾 Nostalgia
29 repositories
🐪 OCaml - js_of_ocaml
3 repositories
🏔 Procedural
Things related to procedural generation, generated worlds, etc.58 repositories
🎲 Property Based Testing
4 repositories
🖼 Shaders
16 repositories
⏱ Staged Programming
8 repositories
🌳 Structural Editing
14 repositories
🏔 World Building - Conlanging
8 repositories
Starred repositories
133
stars
written in Agda
Clear filter
An introduction to programming language theory in Agda
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
An introductory course to Homotopy Type Theory
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Lecture notes on univalent foundations of mathematics with Agda
Categories parametrized by morphism equality, in Agda
Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
Agda formalisation of the Introduction to Homotopy Type Theory
The theory of algebraic graphs formalised in Agda
Algebra of Programming in Agda: Dependent Types for Relational Program Derivation
A workshop on learning Agda with minimal prerequisites.
Abstract binding trees (abstract syntax trees plus binders), as a library in Agda
A cost-aware logical framework, embedded in Agda.
A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
A formalization of the polymorphic lambda calculus extended with iso-recursive types
Inline, type safe X86-64 assembly programming in Agda
A work-in-progress core language for Agda, in Agda
This aims to be the most pretentious implementation of stlc in existence