Andrej Bauer

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

coop. A prototype programming language for programming with runners

Homotopy. Homotopy theory in Coq.

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

faux-type-theory. OCaml

mathematics-and-computation. Andrej Bauer's blog "Mathematics and Computation"

clerical. Command-like expressions for real infinite-precision calculations

what-is-algebraic-about-algebraic-effects. TeX

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

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

miniLCF. A bare-bones LCF-style proof assistant

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

higher-rank-syntax. Lean

hydra. The combinatorial Hydra game

andromeda. A minimalist implementation of type theory, suitable for experimentation

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

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

partial-combinatory-algebras. A Lean 4 formalization of partial combinatory algebras.

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

ppj-skripta. Zapiski pri predmetu Principi programskih jezikov

dependent-type-theory-syntax. An Agda formalization of raw syntax for dependent type theory

lean2sexp. Convert Lean .olean files to s-expressions

ucbenik-logika-in-mnozice. Učbenik za predmet Logika in množice na Fakulteti za matematiko in fiziko, Univerza v Ljubljani

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

lvr-sat. SAT solver (for teaching purposes in the course Logic in computer science)

HoTT. Homotopy type theory

coq-clerical. Coq formalization of Clerical

formalabstracts. Lean

formaltt. Formalization of type theory

type-theory-slovene-dictionary. A dictionary of slovene translations of type-theoretical notions and notions from logic and foundations of mathematics.

TopologyPrimerTest. A test before showing a Lean project to students