Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1994: Types for Proofs and Programs pp 83–100Cite as

A user's friendly syntax to define recursive functions as typed λ-terms

  • Conference paper
  • First Online:

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

Abstract

This paper discusses the problem of translating a (recursive) function definition expressed in a ML like syntax into a typed λ-term. In this paper, we recall how termination proofs can be solutions of the investigated problem. Then we recall how the method of [10] deals with the problem of searching termination proofs. Finally, we discuss the questions raised by the adaptation of our method to 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Barendregt The Lambda Calculus, its Syntax and Semantics; North Holland, 1981, 1984.

    Google Scholar 

  2. C. Cornes et al. The Coq Proof Assistant Reference Manual Version 5.10; Internal Report INRIA.

    Google Scholar 

  3. K. Gödel Über eine bisher noch nicht Erweiterung des finiten Standpunktes; Dialectica 12, 1958.

    Google Scholar 

  4. W. Hodge, B. Watson On a hitherto unexploited extension of finitary standpoint; J.P.L. 9, 1980, english translation of [3].

    Google Scholar 

  5. W.A. Howard The formulæ-as-types notion of construction; in J.R. Hindley, editor, To H.B. Curry: Essays on Combinatory Logic, lambda-calculus and formalism, Seidin, J.P. 1980.

    Google Scholar 

  6. J.L Krivine, M. Parigot Programming with proofs; in SCT 87 (1987), Wendish-Rietz; in EIK 26 (1990) pp 146–167.

    Google Scholar 

  7. P. Martin-Löf Intuitionistic Type Theory; Studies in Proof Theory. Bibliopolis, 1984.

    Google Scholar 

  8. P. Manoury, M. Parigot, M. Simonot ProPre: a programming language with proofs; in proceedings LPAR 92, LNAI 624.

    Google Scholar 

  9. P. Manoury and M. Simonot Des preuves de totalité de fonctions comme synthèse de programmes; Phd Thesis, Université Paris 7, December 1992.

    Google Scholar 

  10. P. Manoury and M. Simonot Automatizing termination proof of recurslvely defined functions; in TCS, 135 (1994), pp 319–343.

    MathSciNet  Google Scholar 

  11. C. Parent Synthese de preuves de programmes dans le Calcul des Constrctions Inductives; PhD thesis, ENS Lyon, January 1995.

    Google Scholar 

  12. M. Parigot Recursive programming with proofs; in TCS 94 (1992) pp 335–356.

    Google Scholar 

  13. C. Paulin-Mohring Inductive Definitions in the System Cog — Rules and properties; proceedings TLCA 93, LNCS 664 (1993).

    Google Scholar 

  14. B. Werner Une théorie des constructions inductives; Phd Thesis, Université Paris 7, May 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Domaine de Voluceau, Rocquencourt, INRIA, F-78153, Le Chesnay Cedex, France

    Pascal Manoury

Authors
  1. Pascal Manoury
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter Dybjer Bengt Nordström Jan Smith

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Manoury, P. (1995). A user's friendly syntax to define recursive functions as typed λ-terms. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-60579-7_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60579-9

  • Online ISBN: 978-3-540-47770-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation