swMATH ID: 7403
Software Authors: Paul Callaghan
Description: 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).
Homepage: http://homepages.inf.ed.ac.uk/wadler/realworld/plastic.html
Related Software: Coq; LEGO; ALF; FraCaS; GF; Nuprl; ML; Twelf; Epigram; Cayenne; Z/EVES; Isabelle
Cited in: 17 Publications

Citations by Year