A type soundness proof for variables in LCF ML

DOI10.1016/0020-0190(95)00146-4zbMATH Open0875.68623OpenAlexW1997282149MaRDI QIDQ672255FDOQ672255

Authors: Juan-Miguel Gracia 

Publication date: 28 February 1997

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(95)00146-4

Recommendations

• Publication:4490735
• scientific article; zbMATH DE number 1670740
• A sound polymorphic type system for a dialect of \(C\)
• A simplified account of polymorphic references
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L

zbMATH Keywords

Type theoryFormal semanticsVariables and assignment

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• Type inference for polymorphic references
• A simplified account of polymorphic references

Cited In (1)

• Title not available (Why is that?)

This page was built for publication: A type soundness proof for variables in LCF ML

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q672255)