Dependently typed logic programming in meta-haskell!
Haskell
Switch branches/tags
Nothing to show
Clone or download
Latest commit 7a17faf May 5, 2012
Permalink
Failed to load latest commit information.
Types first commit May 2, 2012
Example.hs first commit May 2, 2012
Kinds.hs added kinds bug May 5, 2012
LICENSE first commit May 2, 2012
README.textile fixed readme May 2, 2012

README.textile

Dependently typed logic programming in meta-haskell!

Overview

An example of using dependently typed logic programming in haskell’s
type system to do theorem proved template black magic without templates.

Details

A big step semantics for lazy lambda
calculus on types used on class logic programming,
and an Isomorphism class which forces a class and
instances under different data types to be isomorphic
to a GADT with constructors such that we the class
can not be instanced elsewhere with more datatypes.