Skip to main content
SpringerLink
Log in

The Gallina specification language: A case study

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

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

Abstract

We present a proposal for a general-purpose specification language, called Gallina. This language combines in a logically sound way three traditional formalisms, issued from mathematical logic and computer science programming languages: Predicate Calculus, Prolog and Recursion Equations. Gallina may be considered as a syntactical variant of the Calculus of Inductive Constructions, a type theory designed in Project Formel for the purpose of extracting programs from correctness proofs of their specifications. It is used as the theory description language of Coq, the current Proof Assistant developed in this project. In this paper we present the salient features of Gallina by illustrating the full axiomatisation and proof development of a non-trivial property of binary sequences, inspired from a card trick of N. Gilbreath. This case study illustrates the power and naturalness of Gallina as a specification language, and outlines a uniform methodology for conducting inductive proofs of Gallina assertions in the Coq proof assistant.

This research was partially supported by ESPRIT Basic Research Action “TYPES.”

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. R. Boyer, J Moore. “A Computational Logic.” Academic Press (1979).

    Google Scholar 

  2. N.G. de Bruijn. “The mathematical language AUTOMATH, its usage and some of its extensions.” Symposium on Automatic Demonstration, IRIA, Versailles, 1968. Printed as Springer-Verlag Lecture Notes in Mathematics 125, (1970) 29–61.

    Google Scholar 

  3. N.G. de Bruijn. “A survey of the project Automath.” (1980) in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds Seidin J. P. and Hindley J. R., Academic Press (1980).

    Google Scholar 

  4. N.G. de Bruijn. “A riffle shuffle card trick and its relation to quasi crystal theory.” Nieuw Archief Voor Wiskunde 5 3 (1987) 285–301.

    Google Scholar 

  5. R.L. Constable et al. “Implementing Mathematics in the Nuprl System.” Prentice-Hall (1986).

    Google Scholar 

  6. R.L. Constable and N.P. Mendier. “Recursive Definitions in Type Theory.” In Proc. Logic of Programs, Springer-Verlag Lecture Notes in Computer Science 193 (1985).

    Google Scholar 

  7. T. Coquand. “Une théorie des constructions.” Thèse de troisième cycle, Université Paris VII (Jan. 85).

    Google Scholar 

  8. T. Coquand. “Metamathematical Investigations of a Calculus of Constructions.” In “Logic and Computer Science,” ed. P. Odifreddi, Academic Press, 1990, 91–122.

    Google Scholar 

  9. T. Coquand, G. Huet. “Constructions: A Higher Order Proof System for Mechanizing Mathematics.” EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985).

    Google Scholar 

  10. T. Coquand and C. Paulin-Mohring. “Inductively defined types.” International Conference on Computer Logic COLOG-88, Tallinn, Dec. 1988. LNCS 417, P. Martin-Löf and G. Mints eds., pp. 50–66.

    Google Scholar 

  11. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Paulin, B. Werner. “The Coq Proof Assistant User's Guide, Version 5.6.” INRIA Technical Report 134, Dec. 1991.

    Google Scholar 

  12. M. Gardner. Mathematical Recreation column, Scientific American, Aug. 1960.

    Google Scholar 

  13. N. Gilbreath. “Magnetic Colors.” The Linking Ring, 38 5 (July 1958), p. 60.

    Google Scholar 

  14. M. J. Gordon, A. J. Millier, C. P. Wadsworth. “Edinburgh LCF.” Springer-Verlag LNCS 78 (1979).

    Google Scholar 

  15. G. Huet. “The Gilbreath Trick: A case study in Axiomatisation and Proof Development in the Coq Proof Assistant.” INRIA Research Report 1511, Sept. 1991.

    Google Scholar 

  16. C. Paulin-Mohring. “Inductive Definitions in the system Coq: Rules and Properties.” Submitted for publication.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Rocquencourt, B.P. 105, 78153, Le Chesnay Cedex, France

    Gérard Huet

Authors
  1. Gérard Huet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rudrapatna Shyamasundar

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huet, G. (1992). The Gallina specification language: A case study. In: Shyamasundar, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1992. Lecture Notes in Computer Science, vol 652. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56287-7_108

Download citation

  • DOI: https://doi.org/10.1007/3-540-56287-7_108

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56287-0

  • Online ISBN: 978-3-540-47507-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation