Plastic: Typed LF with Inductive Types, Universes, and Coercive Subtyping

Plastic is an implementation in Haskell-98 of Typed LF with various extensions, in the form of a proof assistant. Typed LF is a framework type theory, in which other type theories may be defined (Luo, 1994). Extensions include Inductive Types, Universes, and Coercive Subtyping. It may be regarded as a meta-level version of Lego, with extensions. Plastic is used to test ideas from Durham research, and we plan to use it as a platform for implementing domain-specific reasoning tools.

Plastic is implemented in the higher-order non-strict functional language Haskell, and uses the Happy parser generator. It has a convenient emacs-based interface, courtesy of David Aspinall's generic Proof General. Speed-wise, it compares favourably with similar systems written in strict languages (compiled with GHC).

See also Plastic and Computer Assisted Reasoning Group pages.