Refined environment classifiers: Type- and scope-safe code generation with mutable cells

Oleg Kiselyov, Yukiyoshi Kameyama, Yuto Sudo

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

4 Citations (Scopus)

Abstract

Generating high-performance code and applying typical optimizations within the bodies of loops and functions involves moving or storing open code for later use, often in a different binding environment. There are ample opportunities for variables being left unbound or accidentally captured. It has been a tough challenge to statically ensure that by construction the generated code is nevertheless well-typed and well-scoped: all free variables in manipulated and stored code fragments shall eventually be bound, by their intended binders. We present the calculus for code generation with mutable state that for the first time achieves type-safety and hygiene without ad hoc restrictions. The calculus strongly resembles region-based memory management, but with the orders of magnitude simpler proofs. It employs the rightly abstract representation for free variables, which, like hypothesis in natural deduction, are free from the bureaucracy of syntax imposed by the type environment or numbering conventions. Although the calculus was designed for the sake of formalization and is deliberately bare-bone, it turns out easily implementable and not too bothersome for writing realistic program.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 14th Asian Symposium, APLAS 2016, Proceedings
EditorsAtsushi Igarashi
PublisherSpringer Verlag
Pages271-291
Number of pages21
ISBN (Print)9783319479576
DOIs
Publication statusPublished - 2016
Event14th Asian Symposium on Programming Languages and Systems, APLAS 2016 - Hanoi, Viet Nam
Duration: 2016 Nov 212016 Nov 23

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10017 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other14th Asian Symposium on Programming Languages and Systems, APLAS 2016
CountryViet Nam
CityHanoi
Period16/11/2116/11/23

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Refined environment classifiers: Type- and scope-safe code generation with mutable cells'. Together they form a unique fingerprint.

Cite this