Proving memory management invariants for a language based on linear logic

Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We develop tools for the rigorous formulation and proof of properties of runtime memory management for a sample programming language based on a linear type system. Two semantics are described, 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.

Original languageEnglish (US)
Title of host publicationProc 92 ACM Conf Lisp Funct Program
PublisherPubl by ACM
Pages139-150
Number of pages12
ISBN (Print)0897914813, 9780897914819
DOIs
StatePublished - 1992
EventProceedings of the 1992 ACM Conference on Lisp and Functional Programming - San Francisco, CA, USA
Duration: Jun 22 1992Jun 24 1992

Publication series

NameProc 92 ACM Conf Lisp Funct Program

Other

OtherProceedings of the 1992 ACM Conference on Lisp and Functional Programming
CitySan Francisco, CA, USA
Period6/22/926/24/92

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Proving memory management invariants for a language based on linear logic'. Together they form a unique fingerprint.

  • Cite this

    Chirimar, J., Gunter, C. A., & Riecke, J. G. (1992). Proving memory management invariants for a language based on linear logic. In Proc 92 ACM Conf Lisp Funct Program (pp. 139-150). (Proc 92 ACM Conf Lisp Funct Program). Publ by ACM. https://doi.org/10.1145/141478.141527