Extracting programs with exceptions in an impredicative type system

  • Jean-François Monin
Contributed Lectures
Part of the Lecture Notes in Computer Science book series (LNCS, volume 947)


This paper is about exceptions handling using classical techniques of program extraction. We propose an impredicative formalization in the calculus of constructions and we illustrate the technique on two examples. The first one, though simple, allows us to experiment various techniques. The second one is an adaptation of a bigger algorithm previously developed in Coq by J. Rouyer, namely first order unification. Only small changes were needed in order to get a more efficient program from the original one.


Efficient Program Proof Assistant Inductive Definition Type Prop Program Extraction 
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. 1.
    J-R. Abrial. The B-Book. Prentice Hall, 1994 (in preparation).Google Scholar
  2. 2.
    H.P. Barendregt. Lambda Calculi with Types. In S. Abramsky & al., editors, Handbook of Logic in Computer Science, vol 2, S. Abramsky & al. Eds. Clarendon Press, Oxford, 1992.Google Scholar
  3. 3.
    P. Castéran. Pro[gramm,v]ing with continuations: A development in Coq. Coq contribution, 1993 (available by FTP on Scholar
  4. 4.
    Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.Google Scholar
  5. 5.
    Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88. Springer Verlag, 1990. LNCS 417.Google Scholar
  6. 6.
    E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  7. 7.
    G. Dowek & al. The Coq Proof Assistant User's Guide. version 5.8, INRIA-Rocquencourt et CNRS-ENS Lyon, fév. 1993.Google Scholar
  8. 8.
    J-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, vol 1, pp. 225–296, 1991.Google Scholar
  9. 9.
    J-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge Univ. Press, vol 7, 1990.Google Scholar
  10. 10.
    T. Griffin. A formulae-as-types notion of control. POPL, Orlando, 1990.Google Scholar
  11. 11.
    S. Hayashi, H. Nakano. PX, a Computational Logic. Foudations of Computing, MIT Press, 1988.Google Scholar
  12. 12.
    J.L. Lawall and O. Danvy. Separating Stages in Continuation-Passing Style Transformation. POPL, 1993.Google Scholar
  13. 13.
    C. Morgan. Programming form Specification. Prentice Hall International Series in Computer Science. Prentice Hall, 1990.Google Scholar
  14. 14.
    C. Murthy. An evaluation semantics for classical proofs. LICS, Amsterdam, 1991.Google Scholar
  15. 15.
    C. Paulin-Mohring. Extraction de programmes dans le calcul des constructions. thèse de doctorat de l'université Paris VII, 1989.Google Scholar
  16. 16.
    C. Paulin-Mohring. Inductive Definitions in the system Coq; Rules and Properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA'93. Springer Verlag, 1993. LNCS 664.Google Scholar
  17. 17.
    C. Paulin-Mohring and B. Werner. Synthesis of ML Programs in the system Coq. Journal of Symbolic Computation, 15:607–640, 1993.Google Scholar
  18. 18.
    J. Rouyer. Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. Research Report 1795, INRIA-Lorraine, nov. 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jean-François Monin
    • 1
  1. 1.LAA/EIA/EVP Technopôle AnticipaFrance Télécom CNETLannion CedexFrance

Personalised recommendations