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