Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic

Authors Marcin Benke, Aleksy Schubert, Daria Walukiewicz-Chrzaszcz

Thumbnail PDF


  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Marcin Benke
Aleksy Schubert
Daria Walukiewicz-Chrzaszcz

Cite AsGet BibTex

Marcin Benke, Aleksy Schubert, and Daria Walukiewicz-Chrzaszcz. Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Curry-Howard isomorphism makes it possible to obtain functional programs from proofs in logic. We analyse the problem of program synthesis for ML programs with algebraic types and relate it to the proof search problems in appropriate logics. The problem of synthesis for closed programs is easily equivalent to the proof construction in intuitionistic propositional logic and thus fits in the class of PSPACE-complete problems. We focus further attention on the synthesis problem relative to a given external library of functions. It turns out that the problem is undecidable for unbounded instantiation in ML. However its restriction to instantiations with atomic types only results in a case equivalent to proof search in a restricted fragment of intuitionistic first-order logic, being the core of Sigma_1 level of the logic in the Mints hierarchy. This results in EXPSPACE-completeness for this special case of the ML program synthesis problem.
  • ML
  • program synthesis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Lennart Augustsson, 2005. URL:
  2. Coq Development Team. The Coq Proof Assistant Reference Manual V8.4, March 2012. URL:
  3. Thierry Coquand and Gerard Huet. The calculus of constructions. Information and Computation, pages 95-120, 1988. Google Scholar
  4. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207-212, New York, NY, USA, 1982. ACM. Google Scholar
  5. Edsger Wybe Dijkstra. A Discipline of Programming. Prentice Hall, 1976. Google Scholar
  6. Catherine Dubois. Proving ML type soundness within Coq. In Mark Aagaard and John Harrison, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings, pages 126-144, Berlin, Heidelberg, 2000. Springer. Google Scholar
  7. Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded Combinatory Logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 243-258, Dagstuhl, Germany, 2012. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  8. J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l'arithmetique d'ordre supérieur. PhD thesis, Université Paris VII, 1972. Google Scholar
  9. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1969. Google Scholar
  10. Pierre Letouzey. Coq Extraction, an Overview. In C. Dimitracopoulos A. Beckmann and B. Löwe, editors, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, volume 5028 of Lecture Notes in Computer Science. Springer-Verlag, 2008. Google Scholar
  11. Samuel Linial and E. L. Post. Recursive unsolvability of the deducibility, Tarski’s completeness, and independence of axioms problems of propositional calculus. Bulletin of the American Mathematical Society, vol. 55, p. 50, 1949. Abstract. Google Scholar
  12. Per Martin-Löf. Constructive mathematics and computer programming. In Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175. North-Holland, 1982. Google Scholar
  13. Marvin L. Minsky. Recursive unsolvability of Post’s problem of "Tag" and other topics in theory of Turing machines. Annals of Mathematics, 74(3):437-455, 1961. Google Scholar
  14. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Springer, 2002. Google Scholar
  15. Christine Paulin-Mohring. Fω’s programs from proofs in the calculus of constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press, 1989. Google Scholar
  16. J. C. Reynolds. Towards a theory of type structure. In Ehring et al., editor, Programming Symposium, Proceedings Colloque Sur La Programmation, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer, 1974. Google Scholar
  17. Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. On the Mints hierarchy in first-order intuitionistic logic. In A. Pitts, editor, Foundations of Software Science and Computation Structures 2015, volume 9034 of Lecture Notes in Computer Science, pages 451-465. Springer, 2015. URL:
  18. Helmut Schwichtenberg. The MINLOG system. URL:
  19. W. E. Singletary. Many-one degrees associated with partial propositional calculi. Notre Dame J. Formal Logic, 15(2):335-343, 04 1974. Google Scholar
  20. M.H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149. Elsevier, 2006. Google Scholar
  21. Richard Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9:67-72, 1979. Google Scholar
  22. Nicholas Wirth. Systematic Programming: An Introduction. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1973. Google Scholar