Discover @andrejbauer Open Source projects

Andrej Bauer (@andrejbauer)

andrejbauer

Stars
2,771
Global Rank 10,731 (Top 0.4 %)
Followers 771
Following 4
Registered over 13 years ago
Most used languages

OCaml
34.4 %

TeX
18.8 %

Python
15.6 %

Agda 6.3 %

Coq 3.1 %

Mathematica 3.1 %

Perl
3.1 %

Shell
3.1 %

Lean 3.1 %

Java
3.1 %

Verilog 3.1 %

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

Coq 1

OCaml
1

TeX
1

Lean 2

Mathematica 2

Verilog 2

Agda 3

Perl
7

HTML
11

Shell
36

Java
47

Python
58

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

mathematics-and-computation

Andrej Bauer's blog "Mathematics and Computation"

what-is-algebraic-about-algebraic-effects

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

hydra

The combinatorial Hydra game

kmeans

A demonstration of Ocaml modules & functors for machine learning.

zeroes

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

rz

A tool for automatic generation of specifications based on realizability theory

dependent-type-theory-syntax

An Agda formalization of raw syntax for dependent type theory

ppj-skripta

Zapiski pri predmetu Principi programskih jezikov

formalized-mathematics-in-lean

A graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25

costa-surface

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

slack-to-discord

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

ucbenik-logika-in-mnozice

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

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.

TopologyPrimerTest

A test before showing a Lean project to students