Fritz Henglein
- 1 AHO, A., SETHI, R., AND ULLMAN, J. Comp~lers: Princ~ples, Technzques, and Tools. Addlson- Wesley, Reading, Mass., 1986. Addison-Wes}ey, 1986, Reprinted w~th corrections, March 1988. Google Scholar
- 2 BARENDREGT, H. The Lambda calculus: Its syntax and semantics. In Studies in Logzc and the Foundations of Mathematics, vol 103. North-Holland, Amsterdam, 1984.Google Scholar
- 3 BEN-YELLES, C. Type-assignment in the Lambda-calculus. Ph.D. dissertation, University College, Swansea, UK, 1979.Google Scholar
- 4 BOEHM, H. Type inference in the presence of type abstraction. In Proceedmgs of the SIGPLAN '89 Conference on Programm~ng Language Design and hnplementatlon (June 1989), ACM, ACM Press, New York, 1989, 192-206. Google Scholar
- 5 BURSTALL, R., MACQUEEN, D., AND SANNELLA, D. Hope: An experimental applicative language. In Stanford LISP Conference 1980 (1980), 136-143. Google Scholar
- 6 CARDELLI, L. A semantics of multiple inheritance. Inf. Comput. (Inf. Control), 76 (1988), 138-164. Google Scholar
- 7 CARDELLI, L., AND WEGNER, P. On understanding types, data abstraction and polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471-522. Google Scholar
- 8 CHOU, C. Relaxation processes: Theory, case studies and applications. Master's thesis, UCLA, Feb. 1986. Tech. Rep. CSD-860057.Google Scholar
- 9 CLEMENT, D., DESPEYROUX, J., DESPEYROUX, T., AND KAHN, G. A simple applicative language: Mini-ML. INRIA Centre, Sophia Antipolis, RR No. 529, May 1986.Google Scholar
- 10 CURRY, H. Modified basic functionality in combinatory logic. Dialectica 23 (1969), 83-92.Google Scholar
- 11 CURRY, H., AND FEYS, R. Combinatory Logtc. Vol. I, North-Holland, Amsterdam, 1958.Google Scholar
- 12 CURRY, H., HINDLEY, J., AND SELDIN, J. C"mblnatory Logic. Vol. II, Studies in Logie and the Foundations of Mathematics, North-Holland, Amsterdam, 1972.Google Scholar
- 13 DAMAS, L. Type assignment in programming languages. Ph.D. dissertation, Univ. of Edinburgh, 1984.Google Scholar
- 14 DAMAS, L., AND MILNER, R. Principal type schemes for functional programs. In Proceedings of the 9th Annual ACM Symposzum on Princtples of Programming Languages (Jan. 1982), 207-212. Google Scholar
- 15 D"RRE, J., AND ROUNDS, W. On subsumption and semiunification in feature algebras. In Proceedings of the 1990 IEEE Symposium on Logtc in Computer Science (LICS). IEEE Computer Society Press, 1990, 300-311.Google Scholar
- 16 DWORK, C., KANELLAKIS, P., AND MITCHELL, J. On the sequential nature of unifcation. J. Logic Program. I (1984), 35-50. Google Scholar
- 17 EDER, E. Properties of substitutions and unifications. J. Symb. Comput. I (1985), 31-46. Google Scholar
- 18 GEURTS, L., MEERTENS, L., AND PEMBERTON, S. The ABC Programmer's Handbook. Prentice- Hall, New York, 1990. Google Scholar
- 19 GIANNINI, P., AND RONCHI DELLA ROCCA, S. Characterization of typings in polymorphic type discipline. In Proceedings of the Symposium on Logic in Computer Science (1988). IEEE Computer Society Press, 1988, 61-70.Google Scholar
- 20 GmARD, J. Une extension de l'interpretation de Godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In 2nd Scandinavian Logic Symposium (1971), 63-92. In French.Google Scholar
- 21 GIRARD, J., LAFONT, Y., AND TAYLOR, P. Proofs and Types. Vol. 7, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989. Google Scholar
- 22 HENGLEIN, F. Fast left-linear semiunification. In Proceedings of the Internattonal Conference on Computing and Information. Lecture Notes of Computer Science, vol. 468, Springer- Verlag, New York, 1990. Google Scholar
- 23 HEN6LEIN, F. Polymorphic type inference and semi-unification. Ph.D. dissertation, Rutgers Univ., April 1989. Available as NYU Tech. Rep. 443, May 1989, from New York University, Courant Institute of Mathematical Sciences, Department of Computer Science.Google Scholar
- 24 HENGLEtN, F. Type inference and semi-unification. In Proceedtngs of the ACM Conference on LISP and Functional Programming (LFP) (Snowbird, Utah, July 1988), ACM Press, New York, 1988, 184-197. Google Scholar
- 25 HENGLEIN, F., AND MAIRSON, H. The complexity of type inference for higher-order typed lambda calculi. In Proceedtngs of the 18th ACM Symposium on Principles of Programming Languages (POPL) (Orlando, Fl., Jan. 1991), ACM Press, New York, 1991, 119-130. Google Scholar
- 26 HERBRAND, J. Recherches sur la theorie de la demonstration. In Ecrits logtques de Jacques Herbrand, PUF, Paris, 1968. Th~se de Doctorat d'Etat, Universit~ de Paris, 1930. In French.Google Scholar
- 27 HINDLEY, R. The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146 (Dec. 1969), 29-60.Google Scholar
- 28 HtNDLEY, R., AND SELmN, J. Introduction to Combinators and A-Calculus. Vol. 1, London Mathematical Society Student Texts, Cambridge University Press, 1986. Google Scholar
- 29 HOOPER, P. The undeeidability of the Turing machine immortality problem. Ph.D. dissertation, Harvard Univ., June 1965. Computation Lab. Rep. BL-38; also in J. Symbolic Logic, 1966.Google Scholar
- 30 HUDAK, P., AND WADLER, P., EDS. Report on the Programming Language Haskell. Yale Univ., April 1990.Google Scholar
- 31 HUET, G Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27, 4 (Oct. 1980), 797-821. Google Scholar
- 32 HUET, G. R~solution d'equations dans des langages d'ordre 1, 2,.., omega (Th~se de Doctorat d'Etat). Univ. Paris VII, Sept. 1976.Google Scholar
- 33 JOHNSON, G., AND WALZ, J. A max~mum-fiow approach to anomaly isolation in unificationbased incremental type inference. In Proceedmgs of the 13th Annua! ACM Symposzum on Principles ofProgrammtng Languages (Jan. 1986), ACM, New York, 1986, 44 57. Google Scholar
- 34 KANELLAKIS, P., AND MITCHELL, J. Polymorphic unification and ML typing (extended abstract). In Proceedzngs of the 16th Annual ACM OEympos~um on Prtnctples of Programmmg Languages (Jan 1989), ACM, New York, 1989. Google Scholar
- 35 KANELLAKIS, P, MAIRSON, H., AND MITCHELL, J. Unification and ML type reconstruction. In Computatlonal Logtc Essays zn Honor of Alan Robmson, J.-L. Lassez and G. Plotkin. Eds. MIT Press, 1991.Google Scholar
- 36 KAPUR, D., MUSSER, D., NARENDRAN, P,, AND STILLMAN, J. Semi-unification. Tbeor. Comput. Set. 81, 2 (Apr. 1991), 169 188. Based on paper presented at Conference on Foundations of Software Technology and Theoretzcal Computer Sctence (FST-TCS), Dec. 1988. Google Scholar
- 37 KFOURY, A, AND TWR~, J. Type reconstruction in finite-rank fragments of the polymorphlc A-calculus. In Proceedings of the 5th Annual IEEE OEymposzum on Logzc in Computer Science (LICS) (Phfiadelphla, June 1990), IEEE Computer Society Press, New York, 1990, 2 11.Google Scholar
- 38 KFOURY, A., TIURYN, J., AND URZYCZYN, P. A proper extension of ML with an effective type-assignment. In Proceedtngs of the 15th Annual ACM Symposium on Princtples of Programmmg Languages (Jan. 1988), ACM Press, New York, 58 69. Google Scholar
- 39 KrouRv, A., TIURYN, J., AND URZ~CZYN, P. Computational consequences and partial solutions of a generahzed unification problem. In Proceedmgs of the 4th IEEE Symposium on Loglc in Computer Science (LICS) (June 1989). Google Scholar
- 40 KFOURY, A., TmRYN, J., AND URZ~CZYN, P. ML typabihty ~s DEXPTIME-complete. In Proceedtngs of the 15th Colloqzum on Trees in Algebra and Programming (CAAP) (Copenhagen, May 1990), Lecture Notes in Computer Science, vol. 431, Springer, New York, 1990, 206 220. Google Scholar
- 41 KFOURY, A., TmRYN, J., AND URZY~ZYN, P. The undecidability of the semi-umfication problem. In Proceedings of the 22nd Annual ACM OEymposium on T,beorv of Computatzon (STOC) (Baltimore, Md., May 1990), ACM, New York, 1990, 468 476. Google Scholar
- 42 LASSEZ, J., MAHER, M, AND MARRIOTT, K. Unification revisited. In Foundattons of Dedt~tzve Databases and Loglc Programming, J. Minker, Ed., Morgan Kauffman, Palo Alto, Calif., 1987. Google Scholar
- 43 LEtVANT, D. Polymorphic type inference. In Proceedtng~ of the lOth ACM Symposium on Prtnctples ofProgrammzng Languages (Jan. 1983), ACM, New York, 1983, 88-98. Google Scholar
- 44 LEIB, H. On type inference for object-oriented programming languages. In Proceedings of the 1st Workshop on Computer Sctence Loglc (Oct. 1987), Lecture Notes in Computer Science, vol. 329, Springer, New York, 1987. Google Scholar
- 45 LEIB, H. Decidability of semi-unification in two variables. Tech. Rep. INF-2-ASE-9-89, Siemens, Munich, Germany, July 1989.Google Scholar
- 46 LEIB, H. Semi-unification and type mference for polymorphic recursion. Tech Rep. INF2- ASE-5-89~ Siemens, Munich, Germany, 1989.Google Scholar
- 47 LEIB, H., AND HENGLEIN, F. A decidable case of the semi-umfication problem. In Proceedtngs of the 16th Internattonal Sympostum on Mathematlcal Foundations of Computer Science (MFCS), (Sept. 1991), Lecture Notes in Computer Science, Springer, New York, 1991.Google Scholar
- 48 MAIRSON, H. Deciding ML typabihty is complete for deterministic exponential tlme. In Proceedings of the 17th ACM OEymposium on Prmctples of Programmlng Languages ( POPL ) (Jan. 1990), ACM, New York. 1990. Google Scholar
- 49 MARTELLI, A., AND MONTANARI, U. An efficient unification algorithm. ACM Trans. Program. Lang Syst. 4, 2 (Apr. 1982), 258-282. Google Scholar
- 50 MEEgTENS, L. Incremental polymorphic type checking in B In Proceedings ofthe lOth ACM Symposium on Principles of Programmmg Languages (POPL). ACM, New York, 1983, 265-275. Google Scholar
- 51 MIniER, R. A theory of type polymorphism in programming. J. Comput. Syst. Sct. 17 (1978), 348-375.Google Scholar
- 52 MmNER, R., TOFTE, M., AND HARPER, R. The Definition of Standard ML. MIT Press, 1990. Google Scholar
- 53 M~TCHELL, J. Polymorphic type inference and containment. Inf. Control 76 (1988), 211-249. Google Scholar
- 54 MITCHELL, J. Type systems for programming languages. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed., North-Holland, Amsterdam, 1990. Google Scholar
- 55 MITCHELL, J., AND HARPER, R. The essence of ML. In Proceedtngs of the 15th ACM Symposium on Principles of Programming Languages ( POPL ) (Jan. 1988), ACM, New York, 1988. Google Scholar
- 56 MoRR~S, J. Lambda-Calculus Models ofProgramming Languages. Ph.D. dissertation, MIT, 1968.Google Scholar
- 57 MYCROFT, A. Polymorphic type schemes and recursive definitions. In Proceedings ofthe 6th International Conference on Programming, LNCS 167 (1984). Google Scholar
- 58 M~CROFT, A., AND O'KEEFE, R. A polymorphic type system for PROLOG. Artif. Intell. 23 (1984), 295-307. Google Scholar
- 59 PATERSON, M., AND WEGMAN, W. Linear unification. J. Comput. Syst. Sci. 16 (1978), 158-167.Google Scholar
- 60 PUDL~K, P. On a unification problem related to Kreisel's conjecture. Commentationes Math. Univer. Carohnae 29, 3 (1988), 551 556.Google Scholar
- 61 PURDOM, P. Detecting looping simplifications. In Proceedings of the 2nd Conference on Rewrite Rule Theory and Applications (RTA) (May 1987), Springer, New York, 1987, 54-62. Google Scholar
- 62 REYNOLDS, J. Towards a theory of type structure. In Proceedings of the Programming Symposium. Springer, 1974, 408-425. Google Scholar
- 63 SCHWARTZ, J., DEWAR, R., DUSINSKY, E., AND SCHONBERO, E. Programming with Sets: An Introduction to SETL. Springer, New York, 1986. Google Scholar
- 64 STERHNG, L., AND SHAPmO, E. The Art of PROLOG. MIT Press, 1986.Google Scholar
- 65 TURNER, D. An overview of Miranda. SIGPLANNot. 21, 12 (Dec. 1986), 158-166. Google Scholar
- 66 W~3qD, M. Finding the source of type errors. In Proceedings of the IEEE Symposium on Logtc in Computer Science (June 1986), IEEE, New York, 1986, 38-43. Google Scholar
Index Terms
- Type inference with polymorphic recursion
Recommendations
Polymorphism, subtyping, and type inference in MLsub
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWe present a type system combining subtyping and ML-style parametric polymorphism. Unlike previous work, our system supports type inference and has compact principal types. We demonstrate this system in the minimal language MLsub, which types a strict ...
Polymorphic type inference and abstract data types
Many statically typed programming languages provide an abstract data type construct, such as the module in Modula-2. However, in most of these languages, implementations of abstract data types are not first-class values. Thus, they cannot be assigned to ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...
Comments