Cited By
View all- Hayashi STakayama Y(1994)Lifschitz's logic of calculable numbers and optimizations in program extractionLogic, Language and Computation10.1007/BFb0032391(1-9)Online publication date: 1994
Extended projection—new method to extract efficient programs from constructive proofs
Pages 299 - 312
References
[1]
Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, North-Holland, 1981
[2]
Bates, J.I., "A logic for correct program development'', Ph.D. Thesis, Cornell University, 1979
[3]
Beeson, M., "Foundaiion of Constructive Mathematics", Springer, 1985
[4]
Constable, R.L., "Implemeating Mathematics with the Nuprl Proo/ Development System", Prentice-Hall, 1986
[5]
Coquand, T. and Huet, G., "The Calculus of Constructions", I~formaiion and Compulaiion, 76, pp.95-120, 1988
[6]
Goad, C.A., "Computational Uses of the Manipulation of Formal Proofs", Ph.D. Thesis, Stanford University, 1980
[7]
Hayashi, S. and Nakano, H., "PX- A Computational Logic", The MIT Press, 1988
[8]
Huet, G., "A Uniform Approach to Type Theory" (to be published)
[9]
Howard, W. A., "The Formulas-as-types Notion of Construction", in 'Essays on Combinetory Logic, Lambda Calculus and Formalism', eds. J. P. Seldin and J. R. Hindley, Academic Press, 1980
[10]
NordstrSm, B. and Petersson, K., "Programming in constructive set theory: some examples", Proceedings of 1981 Conference on Functional Programming Language and Computer Architecture, pp.141-153, 1983
[11]
Paulin-Mohring, C., "Extracting F~'s Programs from Proofs in the Calculus of Constructions, 16th Annual A(TM Symposium on Principles of Programming Languages, 1989
[12]
Prawitz, D., "Natural Deduction", Almqvist & Wiksell, 1965
[13]
Sasaki, J., "Eztracting Ej~cient Code From Constructive Proofs", Ph.D. Thesis, Cornell University, 1986
[14]
Sato, M., "Typed Logical Calculus", Technical Report 85-13, Department of Information Science, Faculty of Science, University of Tokyo, 1985
[15]
Sato, M., t4 y: A Concurrent Language Based on Logic and Function", Proceedings of the Fourth International Conference on Logic Programming, The MIT Press, 1987
[16]
Takayama, Y., "QPC: QJ-Based Proof Compiler- Simple Examples and Analysis -", LNCS 300, pp49-63, 1988
[17]
Takayama, Y., "Proof Theoretic Approach to the Extraction of Redundancy-free Realizer Codes", to appear in 1989
Index Terms
- Extended projection—new method to extract efficient programs from constructive proofs
Recommendations
Canonicity of Proofs in Constructive Modal Logic
Automated Reasoning with Analytic Tableaux and Related MethodsAbstractIn this paper we investigate the Curry-Howard correspondence for constructive modal logic in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this ...
Extracting programs from constructive HOL proofs via IZF set-theoretic semantics
IJCAR'06: Proceedings of the Third international joint conference on Automated ReasoningChurch's Higher Order Logic is a basis for proof assistants — HOL and PVS. Church's logic has a simple set-theoretic semantics, making it trustworthy and extensible. We factor HOL into a constructive core plus axioms of excluded middle and choice. We ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 1989 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 November 1989
Check for updates
Qualifiers
- Article
Conference
FPCA89: The International Conference on Functional Programming Languages & Computer Architectures
September 11 - 13, 1989
Imperial College, London, United Kingdom
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 301Total Downloads
- Downloads (Last 12 months)39
- Downloads (Last 6 weeks)7
Reflects downloads up to 14 Dec 2024
Other Metrics
Citations
Cited By
View all- Hayashi STakayama Y(1994)Lifschitz's logic of calculable numbers and optimizations in program extractionLogic, Language and Computation10.1007/BFb0032391(1-9)Online publication date: 1994
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in