Discover @andrejbauer Open Source projects

Andrej Bauer (@andrejbauer)

andrejbauer

Stars
2,735
Global Rank 10,513 (Top 0.4 %)
Followers 743
Following 4
Registered about 13 years ago
Most used languages

OCaml
35.5 %

TeX
16.1 %

Python
16.1 %

Agda 6.5 %

Coq 6.5 %

Mathematica 3.2 %

Java
3.2 %

Lean 3.2 %

Verilog 3.2 %

Perl
3.2 %

HTML
3.2 %
Location 🇸🇮 Slovenia
Country Total Rank 8
Country Ranking

Coq 1

OCaml
1

TeX
1

Lean 2

Mathematica 2

Verilog 2

Agda 3

Perl
5

HTML
11

Java
55

Python
62

plzoo

Programming Languages Zoo

homotopy-type-theory-course

A course on homotopy theory and type theory, taught jointly with Jaka Smrekar

spartan-type-theory

Spartan type theory

marshall

Real number computation software

Homotopy

Homotopy theory in Coq.

coop

A prototype programming language for programming with runners

alg

Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.

notes-on-realizability

Lecture notes on realizability

what-is-algebraic-about-algebraic-effects

mathematics-and-computation

Andrej Bauer's blog "Mathematics and Computation"

dedekind-reals

A formalization of the Dedekind reals in Coq

social-distancing-simulator

An artificial simulation of social distancing in the time of an epidemic.

clerical

Command-like expressions for real infinite-precision calculations

miniLCF

A bare-bones LCF-style proof assistant

higher-rank-syntax

simple-random-art

A simple implementation of Random art in Python. Suitable for teaching and experiments.

repl-in-browser

Implementation of a language interpreter in the browser, using js_of_ocaml.

mathematical-stories

Mathematical stories

kmeans

A demonstration of Ocaml modules & functors for machine learning.

rz

A tool for automatic generation of specifications based on realizability theory

hydra

The combinatorial Hydra game

zeroes

Programs for computing beautiful pictures and animations of zeroes of polynomials.

dependent-type-theory-syntax

An Agda formalization of raw syntax for dependent type theory

ppj-skripta

Zapiski pri predmetu Principi programskih jezikov

ucbenik-logika-in-mnozice

Učbenik za predmet Logika in množice na Fakulteti za matematiko in fiziko, Univerza v Ljubljani

slack-to-discord

Transfer Slack archives to a Discord server on a per-channel basis

costa-surface

Triangulation of Costa's minimal surface with normals, suitable for PovRay rendering

lvr-sat

SAT solver (for teaching purposes in the course Logic in computer science)

lvr-coq

Coq related material for the Logic in computer science course

lean2sexp

Convert Lean .olean files to s-expressions

the-daily-algebra

The daily algebra fact.

jurij

A simple Python application for drawing graphs, useful for teaching and experiments.

backup

Remote backups using ssh and rsync.