Skip to content
an attempt at making a prototype proof checker for experimental purposes
OCaml TeX TypeScript Standard ML Coq Shell Other
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
NOTES
emacs
rules
scripts
src
src2
test
.gitignore
Makefile
Makefile-ocaml-rules
README
myocamlbuild.ml

README

-*- coding: utf-8; fill-column: 87; mode: text; mode: auto-fill -*-

An attempt at making a toy proof checker for experimental purposes

This program encodes the type system TS developed in the paper "A universe
polymorphic type system", by Vladimir Voevodsky, the version dated October,
2012, and attempts to make a toy prototype proof assistant based on it.

Thanks to:

    Vladimir Voevodsky                  for TS and Univalence

    Andrej Bauer                        for advice about coding and
				        suggesting Logical Frameworks (LF) as the
				        way to go

    Bob Harper and Dan Licata           for explaining LF in an intuitive way

    Bob Harper and Christopher Stone    for the type checking algorithms used here
You can’t perform that action at this time.