Beta-reduction as unification

 Access to full text

 Full (PDF)

1. [1] Bass, S. R., 'The undecidability of k-provability', Annals of Pure and Applied Logic, Vol 53, pp 75-102, 1991. 
2. [2] Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, revised edition, North-Holland, Amsterdam, 1984. Zbl0551.03007
3. [3] Farmer, W. M., 'Simple second-order languages for which unification is undecidable', Theoretical Computer Science, Vol 87, pp 25-41, 1991. Zbl0731.03005
4. [4] Cardone, F., and Coppo, M., 'Two extensions of Curry's type inference system', in Logic and Computer Science, ed. P. Odifreddi, APIC series no. 31, pp 19-75, Academic Press, 1990. 
5. [5] Coppo, M., and Dezani-Ciancaglini, M., 'An extension of basic functionality theory for λ-calculus', Notre Dame Journal of Formal Logic, Vol 21, no. 4, pp 685-693, 1980. Zbl0423.03010
6. [6] Coppo, M., and Giannini, P., 'A complete type inference algorithm for simple intersection types', in Proceedings of CAAP '92, 17th Colloquium on Trees in Algebras and Programming, ed. J.-C. Raoult, Rennes, France. LNCS Vol 581, pp 102-123, Springer-Verlag, 1992. 
7. [7] Coppo, M., and Giannini, P., 'Principal Types and Unification For a Simple Intersection Type System', Information and Computation, Vol 122, pp 70-96, 1995. Zbl0834.68063
8. [8] Goldfarb, W. D., 'The undecidability of the second-order unification problem'. Theoretical Computer Science, Vol 13, pp 225-230, 1981. Zbl0457.03006
9. [9] Hindley, J. R., Basic Simple Type Theory, Cambridge Tracts in Theoretical Computer Science 42, Cambridge University Press, 1997. 
10. [10] Kfoury, A. J., 'A linearization of the λ-calculus and an application'. Submitted for publication. 
11. [11] Kfoury, A. J., 'Beta-reduction as unification'. Technical report, Boston University, 96-019, June 1997. Also available at URL: http://www.cs.bu.edu/faculty/kfoury/research.html 
12. [12] Kfoury, A. J., Tiuryn, J., and Urzyczyn, P., 'The undecidability of the semi-unification problem'. Information and Computation, Vol 102, no. 1, pp 83-101, 1993. Zbl0769.68059
13. [13] Kfoury, A. J., and Wells, J. B., 'New Notions of Reduction and Non-Semantic Proofs of Beta Strong Normalization in Typed Lambda Calculi', Proceedings of Logic in Computer Science, June 1995. 
14. [14] Krajíček, J., and Pudlák, P., 'The number of proof lines and the size of proofs in first order logic'. Archive for Mathematical Logic, Vol 27, pp 69-84, 1988. Zbl0644.03032
15. [15] Leivant, D., 'Polymorphic Type Inference', Proceedings of Tenth Annual ACM Symposium on Principles of Programming Languages, pp 88-98, 1983. 
16. [16] Levy, J., 'Linear second-order unification'. In Proceedings of RTA, July 1996. Also available at URL: http://www-lsi.upc.es/~jlevy 
17. [17] Mitchell, J. C., Foundations for Programming Languages, MIT Press, 1996. 
18. [18] Pottinger, G., 'A Type Assignment for the Strongly Normalizable λ-terms', in To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, J.P. Seldin and J.R. Hindley, eds., pp 561-577, Academic Press, 1980. 
19. [19] Schmidt-Schauß, M., 'Unification of stratified second-order terms'. Technical Report, Fachbereich Informatik, Johann Wolfgang-Goethe-Universität Frankfurt, 1996. Author's e-mail: schauss@informatik.uni-frankfurt.de 
20. [20] Schubert, A., 'Second-order unification and type inference for Church-style polymorphism'. Technical Report, Institute of Informatics, Warsaw University, January 1997. Available from FTP site: zls.mimuw.edu.pl in files: pub/alx/simple.dvi.tar.gz and pub/alx/simple.ps.gz. Shorter version in Proceedings of 26th Annual ACM Symposium on Principles of Programming Languages, 1998. 
21. [21] Retoré, C., 'A Note on Intersection Types', INRIA report RR-2431, %January 1995, postscript available at: ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-2431.ps.gz 
22. [22] van Bakel, S., 'Complete restrictions of the intersection type discipline'. Theo. Comp. Sc., Vol 102, pp 135-163, 1992. Zbl0762.03006
23. [23] van Bakel, S., Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. Doctoral dissertation, Catholic University of Nijmegen, also issued by the Mathematisch Centrum, Amsterdam, 1993.