Abstract
We propose a method to search for a lemma in a Coq proof library by using the lemma type as a key. The method is based on the concept of type isomorphism developed within the functional programming framework. We introduce a theory which is a generalization of the axiomatization for the simply typed γ-calculus (associated with Closed Cartesian Categories) to an Extended Calculus of Constructions with a more Extensional conversion rule. We show a soundness theorem for this theory but we notice that it is not contextual and requires “ad hoc” contextual rules. Thus, we see how we must adapt this theory for Coq and we define an approximation of the contextual part of this theory, which is implemented in a decision procedure.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Maria-Virginia Aponte and Roberto Di Cosmo. Type isomorphisms for module signatures. In Programming Languages Implementation and Logic Programming (PLILP), volume 1140 of Lecture Notes in Computer Science, pages 334–346. Springer-Verlag, 1996.
Maria-Virginia Aponte, Roberto Di Cosmo, and Catherine Dubois. Signature subtyping modulo type isomorphisms, 1998. http://www.pps.jussieu.fr/~dicosmo/ADCD97.ps.gz.
Andrew W. Appel et al. Standard ML of New Jersey User’s Guide. New Jersey, 1998. http://cm.bell-labs.com/cm/cs/what/smlnj/doc/index.html.
Bruno Barras et al. The Coq Proof Assistant Reference Manual Version 6.3.1. INRIA-Rocquencourt, May 2000. http://coq.inria.fr/doc-eng.html.
Dave Berry et al. Edinburgh SML. Laboratory for Foundations of Computer Science, University of Edinburgh, 1991. http://www.lfcs.informatics.ed.ac.uk/software/.
Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of type. In Mathematical Structures in Computer Science, volume 2(2), pages 231–247, 1992.
Roberto Di Cosmo. Isomorphisms of Types: from γ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X.
M. J. C. Gordon et al. A metalanguage for interactive proof in LCF. In 5th POPL, ACM, 1978.
Simon Peyton Jones et al. Haskell 98, February 1999. http://www.haskell.org/definition/.
Thomas Kolbe and Christoph Walther. Adaptation of proofs for reuse. In Adaptation of Knowledge for Reuse, AAAI Fall Symposium, 1995. http://www.aic.nrl.navy.mil/~aha/aaai95-fss/papers.html#kolbe.
Thomas Kolbe and Christoph Walther. Proof management and retrieval. In Working Notes of the IJCAI Workshop, Formal Approaches to the Reuse of Plans, Proofs, and Programs, 1995. http://www.informatik.uni-freiburg.de/~koehler/ijcai-95/ijcai-ws/kolbe.ps.gz.
Xavier Leroy. The Caml Light system, documentation and user’s guide Release 0.74. INRIA-Rocquencourt, December 1997. http://caml.inria.fr/man-caml/index.html.
Xavier Leroy et al. The Objective Caml system release 3.00. INRIA-Rocquencourt, April 2000. http://caml.inria.fr/ocaml/htmlman/.
Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, July 1990.
A. Mili, R. Mili, and R. T. Mittermeir. A survey of software reuse libraries. In Annals of Software Engineering, volume 5, pages 349–414, 1998.
Mikael Rittri. Using types as search keys in function libraries. In Journal of Functional Programming, volume 1(1), pages 171–89, 1991.
Sergei Soloviev. The category of finite sets and cartesian closed categories. In Journal of Soviet Mathematics, volume 22(3), pages 154–172, 1983.
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
Delahaye, D. (2000). Information Retrieval in a Coq Proof Library Using Type Isomorphisms. 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_8
Download citation
DOI: https://doi.org/10.1007/3-540-44557-9_8
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