Proving memory management invariants for a language based on linear logic
- 1 January 1992
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. V (1) , 139-150
- https://doi.org/10.1145/141471.141527
Abstract
We develop tools for the rigorous formulation and proof of properties of runtime management for a sample programming language based on a linear type system. Two semantics are diescribed, one at a level of observable results of computations and one describing linear connectives in terms of memory-management primitives. The two semantics are proven equivalent and the memory-management model is proven to satisfy fundamental correctness criteria for reference counts.Keywords
This publication has 11 references indexed in Scilit:
- Operational aspects of linear lambda calculusPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Parameter-passing and the lambda calculusPublished by Association for Computing Machinery (ACM) ,1991
- Is there a use for linear logic?Published by Association for Computing Machinery (ACM) ,1991
- The linear abstract machineTheoretical Computer Science, 1988
- Linear logicTheoretical Computer Science, 1987
- A semantic model of reference counting and its abstraction (detailed summary)Published by Association for Computing Machinery (ACM) ,1986
- A flexible approach to interprocedural data flow analysis and programs with recursive data structuresPublished by Association for Computing Machinery (ACM) ,1982
- Garbage Collection of Linked Data StructuresACM Computing Surveys, 1981
- LCF considered as a programming languageTheoretical Computer Science, 1977
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975