Fritz Henglein. Dynamic Typing: Syntax and Proof Theory. Science of Computer Progamming (SCP), 22(3):197-230, 1994.
Download paper:
Doi page
Download paper:
Adobe portable document (pdf) 
Copyright notice:This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
We present the dynamically typed lambda-calculus, an extension of the statically typed lambda-calculus with a special type Dyn and explicit dynamic type coercions corresponding to run-time type tagging and type check-and-untag operations. Programs in run-time typed languages can be interpreted in the dynamically typed lambda-calculus via a nondeterministic completion process that inserts explicit coercions and type declarations such that a well-typed term results. We characterize when two different completions of the same run-time typed program are coherent with an equational theory that is independent of an underlying I-theory. This theory is refined by orienting some equations to define safety and minimality of completions. Intuitively, a safe completion is one that does not produce an error at run-time which another completion would have avoided, and a minimal completion is a safe completion that executes fewest tagging and check-and-untag operations amongst all safe completions. We show that every untyped lambda-term has a safe completion at any type and that it is unique modulo a suitable congruence relation. Furthermore, we present a rewriting system for generating minimal completions. Assuming strong normalization of this rewriting system we show that every lambda-term has a minimal completion at any type, which is furthermore unique modulo equality in the dynamically typed lambda-calculus
[ Dyntyp ]
@article{henglein94b,
Author = {Henglein, Fritz},
Title = {Dynamic Typing: Syntax and Proof Theory},
Journal = {Science of Computer Progamming (SCP)},
Volume = {22},
Number = {3},
Pages = {197--230},
Publisher = {Elsevier North-Holland, Inc},
Address = {Amsterdam, The Netherlands, The Netherlands},
Year = {1994}
}
Get EndNote Reference (.ref)