Type Error Slicing in Implicitly Typed Higher-Order Languages
型付けに失敗した時にその原因箇所をスライスする手法の論文。 型推論は制約解消なので初めに解くべき制約集合を求める。この時、各制約とプログラム断片を対応付けておく。これにより、制約集合が充足不能だった場合に充足不能な極小部分集合を求め、極小部分集合に含まれる制約に対応づけられたプログラム断片をスライスとして得ることができる。この論文が対象としているのは let 付きの型付きλ。得られたスライスがやはり型付けできないことと、最小のスライスになっていることがちゃんと証明されている。
author="Christian Haack and J.B. Wells",
title="{Type Error Slicing in Implicitly Typed Higher-Order Languages}",
journal="Science of Computer Programming",
volumn="50",
number="1-3",
pages="189--224",
year="2004"