andrejbauer/plzoo

Stars
1,420
Rank 31,887 (Top 0.7 %)
Language
OCaml
License
MIT License
Created over 10 years ago
Updated 2 months ago

andrejbauer/plzoo

andrejbauer

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Programming Languages Zoo

The Programming Languages Zoo

The Programming Languages Zoo, or PL Zoo for short, is a collection of implementations of miniature programming languages which demonstrates various techniques used in implementation of programming languages. It is a good starting point for those who would like to implement their own programming language, or just learn how it is done.

See the PL Zoo website for further information, including installation instructions.

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.