GitHub - kach/prufrock: A literary proof assistant built on the affine calculus of inductive constraints

kach / prufrock Public

Notifications You must be signed in to change notification settings
Fork 0
Star 8

A literary proof assistant built on the affine calculus of inductive constraints

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 15 Commits
Makefile		Makefile
README.txt		README.txt
notes.txt		notes.txt
prelude.pf		prelude.pf
prufcore.sml		prufcore.sml
prufdict.sml		prufdict.sml
prufparse.sml		prufparse.sml
prufrepl.mlb		prufrepl.mlb
prufrepl.sml		prufrepl.sml
sample-output.txt		sample-output.txt

Repository files navigation

Stories are proofs of the present.
Proofs  are types  of the terms.
Terms of what?
Terms of an affine variant of the calculus of inductive constraints.

Prufrock is a literary proof assistant.

(Oh, do not ask, "What is it?"
 Let us go and make our visit.)