Plastic 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 all top 5 Cited by 13 Authors 12 Luo, Zhaohui 3 Adams, Robin 2 Barthe, Gilles 2 Callaghan, Paul T. 2 Luo, Yong 2 McBride, Conor Thomas 2 Solov’ëv, Sergeĭ Vladimirovich 1 Brady, Edwin C. 1 Chatzikyriakidis, Stergios 1 McKinna, James 1 Perrier, Guy 1 Pons, Olivier 1 Xue, Taoxue all top 5 Cited in 6 Serials 2 Information and Computation 2 MSCS. Mathematical Structures in Computer Science 1 Annals of Pure and Applied Logic 1 Journal of Automated Reasoning 1 Journal of Logic, Language and Information 1 ACM Transactions on Computational Logic Cited in 3 Fields 12 Mathematical logic and foundations (03-XX) 12 Computer science (68-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year