Abstract
In the early 80's, V. Lifschitz presented a classical logic which can code up constructive logic [8], [9]. We will show how it is used for optimization in program extraction. We will show that the second author's extended projection method [13], [14] can be considered as a translation of constructive proofs into Lifschitz's logic. We will also give an interpretation of Lifschitz's logic into the first author's type system ATTT, which evolved from the extended projection method.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Constable, R.L. and others: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986
Dowek, C. and others: The Coq Proof Assistant User's Guide, Version 5.6, Technical report, No. 134, INRIA, December, 1991
Hayashi, S.: Singleton, Union and Intersection Types for Program Extraction, Lecture Notes in Computer Science 526 (1991) 701–730
Hayashi, S: Logic of refinement types, in Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, Nijmegen, (1993) 157–172, the formal version of the proceedings is to appear in Springer LNCS.
Hayashi, S. and Nakano, H.: PX: A Computational Logic, The MIT Press, 1988
Hayashi, S. and Takayama, Y.: Extended projection method and realizability interpretation, a talk presented at Workshop on Programming Logic, Bastad, Sweden, 1990
Kreisel, G. and Troelstra, A. S.: Formal Systems for Some Branches of Intuitionistic Analysis, Annals of Math. Logic 1 1970) 229–387
Lifschitz, V.: Calculable Natural Numbers. Intensional Mathematics, S. Shapiro ed. (1985) 173–190, North-Holland
Lifschitz, V.: Constructive Assertions in an Extension of Classical Mathematics. J.S.L. 47 (1982) 359–387
Mints, G. E.: Normalization of Natural Deduction and the effectivity of classical existence, in ”Logicheskii Vyvod”, Moscow, Nauka (1979) 73–77 (in Russian), English translation is in G. E. Mints, Selected Papers in Proof Theory, Biblioplis, Napoli, Italia and North-Holland, Amsterdam, Distributed by North-Holland (1992) 123–146.
Mitchell, J. C.: Type systems for programming languages, in Handbook of Theoretical Computer Science, Volume B, J. van Leeuwen ed., (1990) 365–458, North-Holland
Nordström, B. and Petersson, K. and Smith, J.M.: Programming in Martin-Löf's type theory, an introduction, Clarendon Press, 1990
Takayama, Y.: Extended Projection: a new technique to extract efficient programs from constructive proofs, Proceedings of 1989 Conference on Functional Programming Languages and Computer Architecture, ACM Press, 1989
Takayama, Y.: Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs, Journal of Symbolic Computation 12 (1991) 29–69.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hayashi, S., Takayama, Y. (1994). Lifschitz's logic of calculable numbers and optimizations in program extraction. In: Jones, N.D., Hagiya, M., Sato, M. (eds) Logic, Language and Computation. Lecture Notes in Computer Science, vol 792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032391
Download citation
DOI: https://doi.org/10.1007/BFb0032391
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57935-9
Online ISBN: 978-3-540-48391-5
eBook Packages: Springer Book Archive