GitHub - rdmarsh2/chiso-tex: A program using the Curry-Howard isomorphism to check and produce typeset proofs from a proof term

rdmarsh2 / chiso-tex Public

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

A program using the Curry-Howard isomorphism to check and produce typeset proofs from a proof term

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 11 Commits
src		src
BNF		BNF
LICENSE		LICENSE
README		README
chiso-tex.cabal		chiso-tex.cabal

Repository files navigation

This takes a proof term in a haskell-like concrete syntax and converts it into
a LaTeX-formatted proof of in a termless logic.  Currently supports only the
propositional calculus

TODO: 
	add first-order logic
	generalize and separate the pretty-printer
	clean up the generated latex source