Typability and type checking in the second-order λ-calculus are equivalent and undecidable
- 17 December 2002
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 2, 176-185
- https://doi.org/10.1109/lics.1994.316068
Abstract
No abstract availableThis publication has 16 references indexed in Scilit:
- Type reconstruction in Fω is undecidablePublished by Springer Nature ,2005
- The Undecidability of the Semi-unification ProblemInformation and Computation, 1993
- Type reconstruction in finite rank fragments of the second-order λ-calculusInformation and Computation, 1992
- Finitely stratified polymorphismInformation and Computation, 1991
- Type inference in polymorphic type disciplinePublished by Springer Nature ,1991
- LEAP: A language with eval and polymorphismPublished by Springer Nature ,1989
- The typechecking of programs with implicit type structurePublished by Springer Nature ,1984
- Towards a theory of type structureLecture Notes in Computer Science, 1974
- The Principal Type-Scheme of an Object in Combinatory LogicTransactions of the American Mathematical Society, 1969
- Modified basic functionality in combinatory logicDialectica, 1969