Nada Amin Claim this profile

an incremental approach to compiler construction

LLM verified with Monte Carlo Tree Search

formalization of the Dependent Object Types (DOT) calculus

interactive programming tutorials, powered by Github and Docker

multi-stage relational programming for staged relational interpreters: running with holes, faster

explorations in core.logic

Course on Metaprogramming

Artifact for OOPSLA'16 Paper on Unsoundness of Java and Scala

Collapsing Towers of Interpreters (in Scheme)

the Art of the Propagator

debugging biological networks to reach coherence, completeness and consistency

computer-aided harmony and counterpoint

prototyping logic programming in Scala

CLP(SMT) on top of miniKanren

Python library for program synthesis and symbolic execution combining constraint solving and LLMs

generative programming & verification

purple: compiling a reflective language

Prolog-Style Meta-Interpreters in miniKanren

A Declarative Theorem Prover for First-Order Classical Logic

No description.

Dafny for Metatheory of Programming Languages

Workshop on Program Transformations

CLP(Set) in miniKanren

exploration of reflective architectures in Scheme

Graduated to js.scala: JavaScript as an embedded DSL in Scala

core.logic.nominal at the minikanren confo 2013

piggybacking on the Dafny language implementation to explore interactive semi-automated verified program synthesis, combining LLMs and symbolic reasoning

software archaeology of reflective towers of interpreters

program synthesis with neuro-symbolic differentiable interpreters

Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp

the reflective tower Blond by Olivier Danvy & Karoline Malmkjær

reading and understanding the lua source code

From Greek to Clojure, Clojure/conj 2013

No description.

Code from the paper Reflection for the Masses by Charlotte Herzeel, Pascal Costanza, and Theo D'Hondt.

reflection-oriented programming

various code snippets in various languages

Based on lectures on the LLM-Verifier Interface at the Summer School on Foundations of Programming and Software Systems (FoPSS 2026)

variations on lisp, exploring reflection

No description.

No description.

Practical type inference for arbitrary-rank types

No description.

ICFP 2017 Artifact for Functional Pearl: A Unified Approach to Solving Seven Programming Problems

Synthesis of simple virus-like programs via relational interpreter.

Kenichi Asai's reflective programming language Black

the reflective language(s) Brown by Dan Friedman and Mitch Wand

A Rational Defense of Reasonable Reflection (LICS'26 Keynote)

A modular module system by Xavier Leroy

Eurisko-Inspired Discovery System for Lean in Lean

This is a pip package implementing Reinforcement Learning algorithms in non-stationary environments supported by the OpenAI Gym toolkit.

FOL Software Archaeology

open, extensible composition models

Scala reflection playground, which implements Scala proxies

natural language → argument graph → AF semantics → FOL (TPTP)

Study of Inductive Program Synthesis by Using a Reversible Meta-Interpreter (Numao & Shimura, 1997)

a system for analyzing and repairing arguments

reflective architectures that instrument and reify the computation steps

Common Lisp port of Doug Lenat's EURISKO

Feeling Wheel 2.0: analyze your mood

A simple interpreter featuring a tracing JIT

appendix of Jake Beal's master thesis (2002)

Course Project in Synthesis, Analysis and Verification in Scala

Collapsing Towers for Side-Channel Security

Feel Wheel: analyze your mood

No description.

Original Code for Engineered Robustness by Controlled Hallucination (AAAI 2008) by Beal and Sussman

a heterogeneous reflective tower the meta level is an LLM

Metaprogramming Lecture Notes

No description.

A fast implementation of miniKanren with disequality and absento, compatible with Racket and Chez.

No description.

LCF checks theorem construction; reviser checks belief revision

LCF checks theorem construction; climber checks theory construction

Eurisko-like discovery system in Python

Dafny Verifier Tool for the Model Context Protocol, which can be used with Claude

learn from libraries (e.g. Lean's Mathlib) to rank & score useful premises, old & new

explorations in Lean automation and metaprogramming

No description.

prototyping self-optimizing systems

a prose experiment in learning S-expression manipulations

Scala framework for iterative and interactive cluster computing.

Programming Microsoft Excel

EURISKO-inspired reflection, LCF-style trust — a fixed-gate verified discovery system in Lean 4

multi-stage programming from Scheme to SMT

About This repository holds the scripts that implement Knowledge Graph based Retrieval-Augmented Generation for Large Language Models

Collaborative Programmable Music

egg is a flexible, high-performance e-graph library

a verified reflective tower inspired by Black and CakeML, the mix of grey and green

The Löbian obstacle to self-modifying systems, as Lean 4 theorems

β is a refinement, not an equivalence, under reflection

a calculator whose class of admissible total functions grows with proofs

a verified reflective tower inspired by Black

a Lean 4 mechanization of Wand 1998, The Theory of Fexprs is Trivial

No description.

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

(vibe-coded) Chrome extension to block videos from (dis)playing on Twitter/X

Some Kappa ChatGPT GPT actions to run simulations, with async support for long-running simulations

open-ended argument mapping

Argument Highlighter

Collapsing Towers of Interpreters

Prototype smart text editor

Integration of BMS with medikanren

a Cursor VSCode extension to automatically run a command and feed any error to the Cursor chat window

an io.livecode.ch for OCaml

Learning Formal Mathematics from Intrinsic Motivation

No description.

a ChatGPT plugin to interact with io.livecode.ch, which can be used as a template to create custom ChatGPT plugins and GPT actions

M-x start-hacking

No description.

Library for running a Monte Carlo tree search, either traditionally or with expert policies

No description.

Implicits in Practice (demo at ML Family Workshop 2014)

Relational version of parsing with derivatives code

No description.

Fixing the ChezScheme Socket Example

A system that improves creates new things worth protecting, so its gate must be able to improve with it — this artifact is the proof that it can, safely, at every depth.

corpus generated by lean-eureka

tmp repo to test github app

SC Mini is a "minimal" positive supercompiler (fork with sound LLM rewrites)

from ⊤ to proof: the program wasn’t rewritten; it was understood.

reflective tower with verified conservative extensions (a simplification of lean-sage)

kernel-typed-evidence pattern

Climber checks theory construction; defeater checks theory qualification.

a verified reflective tower inspired by Black and CakeML

a lemmafit app for the equality game, created on the Boston Esplanade in the year 2000

An auto-active verifier embedded into Lean

🦾 Take control of your AI agents

random little scripts I use

Hoare-style verification for programs with holes: computes obligations, checks completions.

Dafny is a verification-aware programming language

No description.

In-browser code editor

A library of examples showing how to use the Common Crawl corpus.

IP Address Viewer

VSCode IDE Integration for Dafny

minimal word count app

No description.

No description.

LLMs as Copilots for Theorem Proving in Lean

No description.

No description.

Get started with building Fullstack Agents using Gemini 2.5 and LangGraph

LLMs + Lean, on your laptop or in the cloud

No description.

Open Source Text Embedding Models with OpenAI Compatible API

A lightweight, powerful framework for multi-agent workflows

✨ Expose any local TCP/IP service on the internet.

LLM based autonomous agent that conducts deep local and web research on any topic and generates a long report with citations.

evaluator for lichess.org puzzles

an io.livecode.ch for Python

Model Context Protocol Servers

Run io.livecode.ch as an MCP server

Take control of your health

AI-Powered Jupyter Notebook built using React

A library to communicate with ChatGPT, Claude, Copilot, Gemini, HuggingChat, and Pi

LDB: A Large Language Model Debugger via Verifying Runtime Execution Step by Step

AIDE: the Machine Learning CodeGen Agent

ChatGPT generated streamlit app

Tool suite for kappa models. Documentation and binaries can be found in the release section. Try it online at

OpenAI-like HTTP server API implementation which supports tool-calling and other structured LLM response generation (e.g. make it conform to a JSON schema)

🦜🔗 Build context-aware reasoning applications

Build system for the RTX-KG2 biomedical knowledge graph, part of the ARAX reasoning system (https://github.com/RTXTeam/RTX)

Examples in the MLX framework

LlamaIndex is a data framework for your LLM applications

Research platform for new language concepts and compiler technologies for Scala.

No description.

ChatGPT plugin for theorem proving in Lean

No description.

Train transformer language models with reinforcement learning.

Metaprogramming in Coq

No description.

A core language for rule-based hardware design 🦑

A rudimentary Racket implementation using RPython

nothing to see: just to play with https://io.livecode.ch without breaking a live page

ClojureCL is a Clojure library for parallel computations with OpenCL.

A modified version of PROSE Tutorial used to support a formative user study

Microsoft Program Synthesis using Examples SDK is a framework of technologies for the automatic generation of programs from input-output examples. This repo includes samples and sample data for the Microsoft Program Synthesis using Example SDK.

No description.

Vagrant Script for CamFlow.

The Flix Programming Language

Solver interface for higher-order functional programs

experiments in diagrams

A miniKanren interpreter... in miniKanren. Relationally run your relations relationally!

This project aim to developp support for music generation in Scala

Library for deep embedding of DSLs based on Scala macros.

The missing package manager for OS X.

Models of Musical Creativity (in Clojure)

miniKanren for interactive tutorials on the web

The Twelf Programming Language (mirror of SVN repository)

An R6RS framework for creating compilers that target C.

A composition library for Overtone.

Relational implementation of the CESK machine

No description.

No description.

Eclipse Plugin for Scalastyle

A Framework for Runtime Code Generation and Compiled DSLs

a async http server base on libuv for Chez Scheme

Lisp code for the textbook "Paradigms of Artificial Intelligence Programming"

code accompanying "DeepBach: a Steerable Model for Bach Chorales Generation" paper