TY - GEN
T1 - Functional in-place update with layered datatype sharing
AU - Konec̃ný, Michal
PY - 2003/5/27
Y1 - 2003/5/27
N2 - Hofmann's LFPL is a functional language with constructs which can be interpreted as referring to heap locations. In this view, the language is suitable for expressing and verifying in-place update algorithms. Correctness of this semantics is achieved by a linear typing. We introduce a non-linear typing of first-order LFPL programs which is more permissive than the recent effect-based typing of Aspinall and Hofmann. The system efficiently infers separation assertions as well as destruction and re-use effects for individual layers of recursive-type values. Thus it is suitable for in-place update algorithms with complicated data aliasing.
AB - Hofmann's LFPL is a functional language with constructs which can be interpreted as referring to heap locations. In this view, the language is suitable for expressing and verifying in-place update algorithms. Correctness of this semantics is achieved by a linear typing. We introduce a non-linear typing of first-order LFPL programs which is more permissive than the recent effect-based typing of Aspinall and Hofmann. The system efficiently infers separation assertions as well as destruction and re-use effects for individual layers of recursive-type values. Thus it is suitable for in-place update algorithms with complicated data aliasing.
UR - http://www.scopus.com/inward/record.url?scp=26844509209&partnerID=8YFLogxK
UR - https://link.springer.com/chapter/10.1007/3-540-44904-3_14
U2 - 10.1007/3-540-44904-3_14
DO - 10.1007/3-540-44904-3_14
M3 - Conference publication
AN - SCOPUS:26844509209
SN - 978-3-540-40332-6
VL - 2701
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 195
EP - 210
BT - International Conference on Typed Lambda Calculi and Applications
PB - Springer
ER -