On the operational interpretation of complex types
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.
KeywordsTheorem Prover Abstract Theory Powerful Mechanism Elimination Rule Inductive Type
Unable to display preview. Download preview PDF.
- [CP88]T.Coquand & C.Paulin:: ”Inductively Defined Types”, Proc. of International Conference on Computer Logic, L.N.C.S. 417,1988.Google Scholar
- [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
- [HHP87]R.Harper & R.Honsell & G.Plotkin: ” A Framework for Defining Logics”, Proc. of LICS'87, 1987.Google Scholar
- [Lu90]Zhaohui Luo: ” An Extended Calculus of Constructions”, Ph.D. Thesis, Univ. of Edinburgh, 1990.Google Scholar
- [Pa89]L.Paulson:” The Foundations of a Generic Theorem Prover”, Journal of Automated Reasoning, Vol. 5, 1989.Google Scholar
- [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
- [PfX9]F.Pfenning: ” Elf: A Language for Logic Definition and Verified Metaprogramming”, Proc. of LICS'89, 1989.Google Scholar