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).

References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Chatzikyriakidis, Stergios; Luo, Zhaohui: Natural language inference in Coq (2014)
  2. Luo, Zhaohui; Soloviev, S.; Xue, Taoxue: Coercive subtyping: theory and implementation (2013)
  3. Luo, Zhaohui: Contextual analysis of word meanings in type-theoretical semantics (2011)
  4. Adams, Robin; Luo, Zhaohui: Weyl’s predicative classical mathematics as a logic-enriched type theory (2010)
  5. Luo, Zhaohui: Manifest fields and module mechanisms in intensional type theory (2009)
  6. Luo, Zhaohui; Adams, Robin: Structural subtyping for inductive types with functorial equality rules (2008)
  7. Adams, Robin; Luo, Zhaohui: Weyl’s predicative classical mathematics as a logic-enriched type theory (2007)
  8. Barthe, Gilles: A computational view of implicit coercions in type theory (2005)
  9. Luo, Zhaohui; Luo, Yong: Transitivity in coercive subtyping (2005)
  10. McBride, Conor: Epigram: Practical programming with dependent types (2005)
  11. Pang, Jian-Min; Callaghan, Paul; Luo, Zhao-Hui: LFTOP: an LF-based approach to domain-specific reasoning (2005) ioport
  12. Brady, Edwin; McBride, Conor; McKinna, James: Inductive families need not store their indices (2004)
  13. Soloviev, Sergei; Luo, Zhaohui: Coercion completion and conservativity in coercive subtyping (2002)
  14. Barthe, Gilles; Pons, Olivier: Type isomorphisms and proof reuse in dependent type theory (2001)
  15. Callaghan, Paul; Luo, Zhaohui: An implementation of LF with coercive subtyping and universes (2001)
  16. Luo, Yong; Luo, Zhaohui: Coherence and transitivity in coercive subtyping (2001)
  17. Perrier, Guy: Intuitionistic multiplicative proof nets as models of directed acyclic graph descriptions (2001)
  18. Callaghan, Paul; Luo, Zhaohui: Implementation techniques for inductive types in Plastic (2000)