Skip to main content
SpringerLink
Log in

On the operational interpretation of complex types

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 560))

  • 134 Accesses

Abstract

Recursive and structured metaprogramming facilities are necessary for large proof development in a generic proof manipulation environment. We show how to define a set of mutually inductive types, abstract theories and abstract data types in a LF-like type theory. By interpreting these complex types in an operational way, we get a powerful mechanism to support large proof development.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. T.Coquand & C.Paulin:: ”Inductively Defined Types”, Proc. of International Conference on Computer Logic, L.N.C.S. 417,1988.

    Google Scholar 

  2. A.Felry & A. Miller: ” Specifying Theorem Provers in a Higher-Order Logic Programming Language”, Proc. of CADE'88, L.N.C.S. 310,1988.

    Google Scholar 

  3. R.Harper & R.Honsell & G.Plotkin: ” A Framework for Defining Logics”, Proc. of LICS'87, 1987.

    Google Scholar 

  4. Zhaohui Luo: ” An Extended Calculus of Constructions”, Ph.D. Thesis, Univ. of Edinburgh, 1990.

    Google Scholar 

  5. L.Paulson:” The Foundations of a Generic Theorem Prover”, Journal of Automated Reasoning, Vol. 5, 1989.

    Google Scholar 

  6. K.Petersson: ” A Set Constructor for Inductive Sets in Martin-Lof Type Theory”, Proc. of Category Method in Computer Science, L.N.C.S. 389,1898.

    Google Scholar 

  7. F.Pfenning: ” Elf: A Language for Logic Definition and Verified Metaprogramming”, Proc. of LICS'89, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Changsha Institute of Technology, 410073, Changsha, Hunan, P.R.China

    Qing-Ping Tan & Huo-Wang Chen

Authors
  1. Qing-Ping Tan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Huo-Wang Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Somenath Biswas Kesav V. Nori

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tan, QP., Chen, HW. (1991). On the operational interpretation of complex types. In: Biswas, S., Nori, K.V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1991. Lecture Notes in Computer Science, vol 560. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54967-6_61

Download citation

  • DOI: https://doi.org/10.1007/3-540-54967-6_61

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54967-3

  • Online ISBN: 978-3-540-46612-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation