Abstract
Although type inference for dependent types is in general undecidable, people experience that the algorithms for type inference in Elf programming language stop in common cases. The present paper is a partial explanation of this behaviour. It shows that for a wide range of terms — terms that correspond to first-order logic proofs — the formalism of dependent types gives decidable type inference. We remark also that imposing that the context and the type of a judgement are first-order is not sufficient for obtaining decidability.
This work was supported by Polish national research funding agency KBN grant no. 8 T11C 035 14.
Chapter PDF
References
Gilles Dowek, The undecidability of typability in the lambda-pi-calculus, Typed Lambda Calculi and Applications (M. Bezem and J.F. de Groote, eds.), LNCS, no. 664, 1993, pp. 139–145.
W. D. Goldfarb, The undecidability of the second-order unification problem, TCS (1981), no. 13, 225–230.
R. Harper, F. Honsell, and G. Plotkin, A Framework for Defining Logics, Proceedings of Logic in Computer Science, 1987, pp. 194–204.
G. Huet and B. Lang, Proving and applying program transformations expressed with second order patterns, Acta Informatica (1978), no. 11, 31–55.
Frank Pfenning, Logic Programming in the LF Logical Framework, Logical Frameworks (Gherard Huet and Gordon Plotkin, eds.), Cambridge University Press, 1991.
A. Schubert, Second-order unification and type inference for church-style polymorphism, Proc. of POPL, 1998.
M.H. Sørensen and P. Urzyczyn, Lectures on Curry-Howard Isomorphism, Tech. Report 14, DIKU, 1998.
A.S. Troelstra and D. van Dalen, Constructivism in Mathematics, An Introduction, Volume II, Studies in Logic and the Foundations of Mathematics, vol. 123, North-Holland, 1988.
Stefan van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, and Pawe Urzyczyn, Comparing cubes of typed and type assignment systems, Annals of Pure and Applied Logic (1997), no. 86, 267–303.
Andrei Voronkov, Proof search in intuitionistic logic based on constraint satisfaction, Theorem Proving with Analytic Tableaux and Related Methods (Terrasini, Palermo) (P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, eds.), LNAI, no. 1071, Springer Verlag, 1996, pp. 312–329.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schubert, A. (2000). Type Inference for First-Order Logic. In: Tiuryn, J. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2000. Lecture Notes in Computer Science, vol 1784. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46432-8_20
Download citation
DOI: https://doi.org/10.1007/3-540-46432-8_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67257-9
Online ISBN: 978-3-540-46432-7
eBook Packages: Springer Book Archive