Skip to content

Instantly share code, notes, and snippets.

View gabriel-fallen's full-sized avatar

Alexander Chichigin gabriel-fallen

  • Kontur
  • Tbilisi, Georgia
View GitHub Profile
@hirrolot
hirrolot / a-preface.md
Last active June 14, 2025 16:46
A complete implementation of the positive supercompiler from "A Roadmap to Metacomputation by Supercompilation" by Gluck & Sorensen

This is the predecessor of Mazeppa.

Supercompilation is a deep program transformation technique due to V. F. Turchin, a prominent computer scientist, cybernetician, physicist, and Soviet dissident. He described the concept as follows [^supercompiler-concept]:

A supercompiler is a program transformer of a certain type. The usual way of thinking about program transformation is in terms of some set of rules which preserve the functional meaning of the program, and a step-by-step application of these rules to the initial program. ... The concept of a supercompiler is a product of cybernetic thinking. A program is seen as a machine. To make sense of it, one must observe its operation. So a supercompiler does not transform the program by steps; it controls and observes (SUPERvises) the running of the machine that is represented by th

@hirrolot
hirrolot / terminating-NbE.ml
Last active March 31, 2025 19:47
Terminating untyped NbE with a configurable limit
module Make_term (S : sig
type 'a t [@@deriving show]
end) =
struct
type t = def S.t
and def = Lam of t | Var of int | Appl of t * t
[@@deriving show { with_path = false }]
let _ = S.show
@hirrolot
hirrolot / cps-eval.ml
Last active March 27, 2025 12:49
A simple CPS evaluation as in "Compiling with Continuations", Andrew W. Appel
type cps_var =
(* Taken from the lambda term during CPS conversion. *)
| CLamVar of string
(* Generated uniquely during CPS conversion. *)
| CGenVar of int
type cps_term =
| CFix of (cps_var * cps_var list * cps_term) list * cps_term
| CAppl of cps_var * cps_var list
| CRecord of cps_var list * binder
@hirrolot
hirrolot / a-main.ml
Last active June 17, 2025 15:45
A simple CPS conversion as in "Compiling with Continuations", Andrew W. Appel
(* A variable identifier of the lambda language [term]. *)
type var = string [@@deriving eq]
(* The lambda language; direct style. *)
type term =
| Var of var
| Fix of (var * var list * term) list * term
| Appl of term * term list
| Record of term list
| Select of term * int
@hirrolot
hirrolot / CoC.ml
Last active August 30, 2025 01:15
How to implement dependent types in 80 lines of code
type term =
| Lam of (term -> term)
| Pi of term * (term -> term)
| Appl of term * term
| Ann of term * term
| FreeVar of int
| Star
| Box
let unfurl lvl f = f (FreeVar lvl)
@hirrolot
hirrolot / CoC.ml
Last active August 22, 2025 04:35
Barebones lambda cube in OCaml
(* The syntax of our calculus. Notice that types are represented in the same way
as terms, which is the essence of CoC. *)
type term =
| Var of string
| Appl of term * term
| Binder of binder * string * term * term
| Star
| Box
and binder = Lam | Pi
@suhr
suhr / proofs.md
Last active December 8, 2022 13:05

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.

@martinchapman
martinchapman / mosaic.sh
Last active May 18, 2023 15:25
Visualise a latex document git history
# Visualise a latex document git history
# loop through commits, create a PDF from your main file for each
# translate the pages of that PDF to a single image
# create GIF/mp4 from the folder of images created
# run within your local repository
# prerequisites: ImageMagick and FFmpeg
# create output folder
@ryanbehdad
ryanbehdad / venv.md
Last active September 6, 2025 11:42
Python venv cheat sheet

Python venv virtual environment cheat sheet

Create a venv

To create a virtual environment, go to the root of your project and run

python -m venv venv

It will create a virtual environment called venv

Activate venv

.\venv\Scripts\activate