Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:LFPL with Types for Deep Sharing
Authors: Michal Konecny
Date:Nov 2002
Publication Title:TLCA 2003
First-order LFPL is a functional language for non-size increasing computation with an operational semantics that allows in-place update. The semantics is correct for all well-typed programs thanks to linear restrictions on the typing. Nevertheless, the linear typing is very strict and rejects many correct, natural in-place update algorithms. Aspinall and Hofmann added usage aspects to variables in LFPL terms in order to typecheck more programs while keeping correctness. We further extend this language to typecheck even more programs, especially those that use data sharing on the heap. We do it by assigning usage aspects to certain type subterms instead of whole types thus referring to value portions instead of the whole values. The usage aspects express preconditions of separation between certain argument portions, the guarantees of preservation of certain argument portions and containment of every result portion in some set of argument portions and a rely-precondition for every separation guarantee within the result value. The new typing allows deterministic type-checking with automatic synthesis of the best usage aspects for recursively defined functions.
2002 by Michal Konecny, University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
author = { Michal Konecny },
title = {LFPL with Types for Deep Sharing},
year = 2002,
month = {Nov},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh