Loading...
Please wait, while we are loading the content...
Similar Documents
How to prove type soundness of Java-like languages without forgoing big-step semantics
| Content Provider | ACM Digital Library |
|---|---|
| Author | Ancona, Davide |
| Abstract | Small-step operational semantics is the most commonly employed formalism for proving type soundness of statically typed programming languages, because of its ability to distinguish stuck from non-terminating computations, as opposed to big-step operational semantics. Despite this, big-step operational semantics is more abstract, and more useful for specifying interpreters. In previous work we have proposed a new proof technique to prove type soundness of a Java-like language expressed in terms of its big-step operational semantics. However the presented proof is rather involved, since it requires showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a specific distance function. In this paper we propose a more direct and abstract approach that exploits a standard and general compactness property of the metric space of values, that allows approximation of the coinductive big-step semantics in terms of the small-step one; in this way type soundness can be proved by standard mathematical induction. |
| Starting Page | 1 |
| Ending Page | 6 |
| Page Count | 6 |
| File Format | |
| ISBN | 9781450328661 |
| DOI | 10.1145/2635631.2635846 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2014-07-28 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Coinduction Java Operational semantics Type soundness |
| Content Type | Text |
| Resource Type | Article |
