Abstract
In the context of Plastic, a proof assistant for a variant of Martin-Löf’s Logical Framework LF with explicitly typed γ-abstractions, we outline the technique used for implementing inductive types from their declarations. This form of inductive types gives rise to a problem of non-linear pattern matching; we propose this match can be ignored in well-typed terms, and outline a proof of this. The paper then explains how the inductive types are realised inside the reduction mechanisms of Plastic, and briefly considers optimisations for inductive types.
This work is supported by the University of Durham Mathematical Vernacular project funded by the Leverhulme Trust (http://www.dur.ac.uk/CARG/mv.html) and by the project on Subtyping, Inheritance, and Reuse, funded by UK EPSRC (GR/K79130, see http://www.dur.ac.uk/CARG/sir.html).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
David Aspinall. Proof General WWW Site. http://www.dcs.ed.ac.uk/home/-proofgen.
P. Callaghan. Coherence Checking of Coercions in Plastic. In Proc. Workshop on Subtyping & Dependent Types in Programming, July 2000.
P. Callaghan and Z. Luo. Mathematical vernacular in type theory based proof assistants. User Interfaces for Theorem Provers (UITP’98), Eindhoven, 1998.
Paul Callaghan and Zhaohui Luo. Plastic: an Implementation of LF with Coercive Subtyping & Universes. Journal of Automated Reasoning (Special Issue on Logical Frameworks), 2000. (to appear).
C. Coquand and Th. Coquand. Structured type theory. In Proc. Workshop on Logical Frameworks and Meta-languages (LFM’99), 1999.
Th. Coquand and Ch. Paulin-Mohring. Inductively defined types. Lecture Notes in Computer Science, 417, 1990.
P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.
E. Gimènez. Structural Recursive Definitions in Type Theory. In Proceedings of ICALP’98, volume 1443 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.
A. Jones, Z. Luo, and S. Soloviev. Some proof-theoretic and algorithmic aspects of coercive subtyping. Types for proofs and programs (eds, E. Gimenez and C. Paulin-Mohring), Proc. of the Inter. Conf. TYPES’96, LNCS 1512, 1998.
Z. Luo. A unifying theory of dependent types: the schematic approach. Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver’92), LNCS 620, 1992. Also as LFCS Report ECS-LFCS-92-202, Dept. of Computer Science, University of Edinburgh.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994.
Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, 1999.
Z. Luo and P. Callaghan. Mathematical vernacular and conceptual well-formedness in mathematical language. Proceedings of the 2nd Inter. Conf. on Logical Aspects of Computational Linguistics, LNCS/LNAI 1582, 1998.
L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Types for Proof and Programs, LNCS, 1994.
C. McBride. Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh, 2000.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, 1990.
L. C. Paulson. A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definitions On page: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/docs.html, 1999.
S. L Peyton Jones et al. GHC Haskell Compiler WWW Site.. http://www.haskell.org/ghc.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Callaghan, P., Luo, Z. (2000). Implementation Techniques for Inductive Types in Plastic. In: Coquand, T., Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1999. Lecture Notes in Computer Science, vol 1956. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44557-9_6
Download citation
DOI: https://doi.org/10.1007/3-540-44557-9_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41517-6
Online ISBN: 978-3-540-44557-9
eBook Packages: Springer Book Archive