On the operational interpretation of complex types

  • Qing-Ping Tan
  • Huo-Wang Chen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 560)


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.


Theorem Prover Abstract Theory Powerful Mechanism Elimination Rule Inductive Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [CP88]
    T.Coquand & C.Paulin:: ”Inductively Defined Types”, Proc. of International Conference on Computer Logic, L.N.C.S. 417,1988.Google Scholar
  2. [FM88]
    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. [HHP87]
    R.Harper & R.Honsell & G.Plotkin: ” A Framework for Defining Logics”, Proc. of LICS'87, 1987.Google Scholar
  4. [Lu90]
    Zhaohui Luo: ” An Extended Calculus of Constructions”, Ph.D. Thesis, Univ. of Edinburgh, 1990.Google Scholar
  5. [Pa89]
    L.Paulson:” The Foundations of a Generic Theorem Prover”, Journal of Automated Reasoning, Vol. 5, 1989.Google Scholar
  6. [Pe89]
    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. [PfX9]
    F.Pfenning: ” Elf: A Language for Logic Definition and Verified Metaprogramming”, Proc. of LICS'89, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Qing-Ping Tan
    • 1
  • Huo-Wang Chen
    • 1
  1. 1.Department of Computer ScienceChangsha Institute of TechnologyChangsha, HunanP.R.China

Personalised recommendations