Abstract
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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J-R. Abrial. The B-Book. Prentice Hall, 1994 (in preparation).
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.
P. Castéran. Pro[gramm,v]ing with continuations: A development in Coq. Coq contribution, 1993 (available by FTP on ftp.inria.fr).
Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.
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.
E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.
G. Dowek & al. The Coq Proof Assistant User's Guide. version 5.8, INRIA-Rocquencourt et CNRS-ENS Lyon, fév. 1993.
J-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, vol 1, pp. 225–296, 1991.
J-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge Univ. Press, vol 7, 1990.
T. Griffin. A formulae-as-types notion of control. POPL, Orlando, 1990.
S. Hayashi, H. Nakano. PX, a Computational Logic. Foudations of Computing, MIT Press, 1988.
J.L. Lawall and O. Danvy. Separating Stages in Continuation-Passing Style Transformation. POPL, 1993.
C. Morgan. Programming form Specification. Prentice Hall International Series in Computer Science. Prentice Hall, 1990.
C. Murthy. An evaluation semantics for classical proofs. LICS, Amsterdam, 1991.
C. Paulin-Mohring. Extraction de programmes dans le calcul des constructions. thèse de doctorat de l'université Paris VII, 1989.
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.
C. Paulin-Mohring and B. Werner. Synthesis of ML Programs in the system Coq. Journal of Symbolic Computation, 15:607–640, 1993.
J. Rouyer. Développement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. Research Report 1795, INRIA-Lorraine, nov. 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monin, JF. (1995). Extracting programs with exceptions in an impredicative type system. In: Möller, B. (eds) Mathematics of Program Construction. MPC 1995. Lecture Notes in Computer Science, vol 947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60117-1_19
Download citation
DOI: https://doi.org/10.1007/3-540-60117-1_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60117-3
Online ISBN: 978-3-540-49445-4
eBook Packages: Springer Book Archive