Constructive system for automatic program synthesis
作者： Didier Galmiche
DOI: 10.1016/0304-3975(90)90199-R
关键词:
摘要: Abstract This paper describes a constructive system, based on particular typed λ-calculus with constants and λ-expressions as types. theory is principally intuitionistic type the general idea of programming proofs which means extracting programs from proofs. It can be considered basis system for automatized program sythesis by developing adapted techniques programmation. allows to partially automate construction different specifications type-driven strategy. Moreover, corresponding logical appears like good base higher-order calculus.
elsevier.com
sci-hub.se 参考文章(21)
Susumu Hayashi, PX: a system extracting programs from proofs. Formal Description of Programming Concepts. pp. 399- 424 ,(1987)
M. J. Beeson, Formalizing constructive mathematics: Why and how? Springer, Berlin, Heidelberg. pp. 146- 190 ,(1981) , 10.1007/BFB0090733
Arend Heyting, Intuitionism: An introduction ,(1956)
Errett Bishop, Mathematics as a Numerical Language Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968. ,vol. 60, pp. 53- 71 ,(1970) , 10.1016/S0049-237X(08)70740-7
M. Parigot, J.-L. Krivine, Programming with proofs Journal of Automata, Languages and Combinatorics. ,vol. 26, pp. 149- 167 ,(1990)
R. P. Nederpelt, An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus conference on automated deduction. pp. 182- 194 ,(1980) , 10.1007/3-540-10009-1_15
Masahiko Sato, Theory of symbolic expressions, I Theoretical Computer Science. ,vol. 22, pp. 19- 55 ,(1983) , 10.1016/0304-3975(83)90137-8
C. A. Goad, Proofs as descriptions of computation 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980. pp. 39- 52 ,(1980) , 10.1007/3-540-10009-1_4
A. Kolmogoroff, Zur Deutung der intuitionistischen Logik Mathematische Zeitschrift. ,vol. 35, pp. 58- 65 ,(1932) , 10.1007/BF01186549
Jean-Yves Girard, The system F of variable types, fifteen years later Theoretical Computer Science. ,vol. 45, pp. 159- 192 ,(1986) , 10.1016/0304-3975(86)90044-7