Informatics Report Series


Report   

EDI-INF-RR-0151


Related Pages

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

Home
Title:Typing with Conditions and Guarantees in LFPL
Authors: Michal Konecny
Date:Oct 2002
Publication Title:Types 2002 Workshop Proceedings
Publication Type:Conference Paper
Abstract:
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. We investigate a general approach to easing the tight linear restrictions of LFPL by generalising the static analysis used by Aspinall & Hofmann [2002]. It consists in devising new type systems for the core language of LFPL whose judgements express sets of rely-guarantee pairs with assertions about the operational semantics, namely about the heap representation of the arguments and the result. The method can be applied to other functional languages with heap based operational semantics. As an example and application of the approach we reformulate the language of Aspinall & Hofmann [2002] from this perspective and prove the correctness of some of its crucial typing rules, show its type inference algorithm and the existence of principal types relative to the simple LFPL typing. We refer to other languages based on LFPL which fit into the approach.
Copyright:
2002 by Michal Konecny, University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
@InProceedings{EDI-INF-RR-0151,
author = { Michal Konecny },
title = {Typing with Conditions and Guarantees in LFPL},
book title = {Types 2002 Workshop Proceedings},
year = 2002,
month = {Oct},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh