I detta dokument behandlas frågan om att på ett säkert sätt kombinera beräkningseffekter och flerstegsprogrammering. Vi föreslår ett typsystem, som utnyttjar ett begrepp av stängd typ, för att statiskt kontrollera att ett imperativt flerstegsprogram inte orsakar run-time fel. Vårt tillvägagångssätt demonstreras formellt för ett kärnspråk som kallas MiniML meta ref. Detta kärnspråk säkert kombinerar flera steg konstruktioner och ML-stil referenser, och är en konservativ förlängning av MiniML ref, en enkel imperativ delmängd av SML. I tidigare arbete introducerade vi en sluten typ konstruktör, som var tillräckligt för att säkerställa en säker körning av dynamiskt genererad kod i det rena fragmentet av MiniML meta ref.
Calcagno, Moggi och Sheard utvecklade ett ljudsystem för en flerstegsanalys med referenser med slutna typer REF.
Closed Types for a Safe Imperative MetaML
{'venue': 'UNDER CONSIDERATION FOR PUBLICATION IN J. FUNCTIONAL PROGRAMMING', 'journal': None, 'mag_field_of_study': ['Computer Science']}