Skip to content

Instantly share code, notes, and snippets.


Andrej Bauer andrejbauer

View GitHub Profile
andrejbauer / gist:4272538
Created Dec 12, 2012
A lemma which explains how transport and function extensionalty interact.
View gist:4272538
Variable A : Type.
Variable P : A -> Type.
Variable Q : forall x, P x -> Type.
Lemma transport_funext (f g : forall x, P x) (n : forall x, Q x (f x)) (E : forall x, f x = g x) (x : A) :
(transport (fun h => forall x, Q x (h x)) (funext E) n) x = transport (Q x) (E x) (n x).
andrejbauer / assoc.elf
Created Jun 18, 2013
Twelf seems very finicky about certain details. Here I explore how associative lists depend in unreasonable ways on the complexity of the value type.
View assoc.elf
% Testing how lookup in an associative list works.
% We consider associative lists with keys of type key and values
% of type value.
% Ideally, we want key to be any type with decidable
% equality and value to be any type. However, we use natural numbers
% as keys so that we can convince Twelf that key has decidable equality.
% Is there a way to tell Twelf "assume key has decidable equality"?
andrejbauer /
Created Dec 28, 2013
A simple program to compute the Mandelbrot set.
(* The Mandelbrot set.
Compile with:
ocamlbuild mandelbrot.native
Example usage:
./mandelbrot.native --xmin 0.27085 --xmax 0.27100 --ymin 0.004640 --ymax 0.004810 --xres 1000 --maxiter 1024 --file pic.ppm
andrejbauer / example.m31
Last active Aug 6, 2016
Example of Andromeda ML-programming
View example.m31
(* In Andromeda everything the user writes is "meta-level programming. *)
(* ML-level natural numbers *)
mltype rec mlnat =
| zero
| succ of mlnat
(* We can use the meta-level numbers to define a program which computes n-fold iterations
of f. Here we give an explicit type of iterate because the ML-type inference cannot tell
andrejbauer / README.markdown
Last active Feb 4, 2017
Elimination of constants and function symbols from set theory
View README.markdown

Official Zermelo-Fraenkel set theory only has the elementhood relation symbol ∈, and nothing else. Other constants, such as ∅, ⊆, ∩, ∪, f[x], etc. can be mechanically eliminated. The result of the elimination is a formula which is logically equivalent to the original, but is more complicated.

This program eliminates constants and function symbols, and generates LaTeX showing the formula before and after the elimination.

andrejbauer / functional2tree.eff
Created Apr 19, 2018
Use of effects and handlers to compute the tree representation of a functional.
View functional2tree.eff
(** This code is compatible with Eff 5.0, see *)
(** We show that with algebraic effects and handlers a total functional
[(int -> bool) -> bool] has a tree representation. *)
(* A tree representation of a functional. *)
type tree =
| Answer of bool
| Question of int * tree * tree
andrejbauer /
Last active May 2, 2018
Experiments in using multicore OCaml effects to simulate dynamically created local effects.
(** * General support for creation of dynamic effects *)
(** We show how to use the multicore Ocaml effects to dynamically generate local
effects. Such effects are akin to the Eff resources, and they can be used to
implement ML references.
The code is based on "Eff directly in OCaml" by Oleg Kiselyov and KC
Sivaramakrishnan ( It was written by
Andrej Bauer, Oleg Kiselyov, and Stephen Dolan at the Dagstuhl seminar
"Algebraic Effect Handlers go Mainstream". *)
andrejbauer / Graph.v
Last active Jan 28, 2019
Graph theory in Coq
View Graph.v
(** An attempt to formalize graphs. *)
Require Import Arith.
(** In order to avoid the intricacies of constructive mathematics,
we consider finite simple graphs whose sets of vertices are
natural numbers 0, 1, , ..., n-1 and the edges form a decidable
relation. *)
(** We shall work a lot with statements of the form
andrejbauer /
Created Aug 14, 2019
Pictures of algebraic numbers
# Compute algebraic numbers in the complex plane and draw a nice picture
import numpy
import sys
import argparse
import math
import cairo
import pickle
andrejbauer / ConstructibleNumbers.nb
Last active Oct 3, 2019
Generation of constructible numbers in Mathematica
View ConstructibleNumbers.nb
(* Content-type: application/vnd.wolfram.mathematica *)
(*** Wolfram Notebook File ***)
(* *)
(* CreatedBy='Mathematica 11.2' *)
(*CacheID: 234*)
(* Internal cache information:
You can’t perform that action at this time.