© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Limits of ML-definability
Stefan Kahrs
In Proceedings of PLILP'96, volume 1140 of Lecture Notes in Computer Science, pages 182-196. Springer, September 1996.Abstract
It is well-known that the type system of ML is overly restrictive in its handling of recursion: certain intuitively sound \emph{terms} do not pass ML's type-check. We formalise this intuition and show that the restriction is semantical: there are computable (semantical) \emph{functions} which cannot be expressed by well-typed (syntactical) terms.
Download publication 52 kbytesBibtex Record
@conference{561,
author = {Stefan Kahrs},
title = {Limits of {ML}-definability},
month = {September},
year = {1996},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1996/561},
booktitle = {Proceedings of PLILP'96},
publisher = {Springer},
refereed = {yes},
series = {Lecture Notes in Computer Science},
volume = {1140},
}