Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable

Wells, J. B. (1994). Typability and Type Checking in the Second-Order Lambda-Calculus Are Equivalent and Undecidable. Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), 176-185.

Type

Conference paper

Intellectual base

Primary research

Year

1994

DOI

10.1109/lics.1994.316068

Link

https://doi.org/10.1109/LICS.1994.316068

Cited from

computer_science

Cited by

1 citation across 1 artifact.

Each citation links to the sentence it supports in the citing article.

Primes

• Computability
  • word problems in finitely presented groups; provability predicates. Computer science. Verification limits via Rice's theorem (no algorithm decides non-trivial semantic properties of arbitrary programs); undecidable type systems

    This sourceProves type inference for System F (second-order lambda calculus) undecidable, an instance of undecidable type systems.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:62316c3d272d · see in the full table