%0 Journal Article 
%F henglein94b
%A Henglein, Fritz
%T Dynamic Typing: Syntax and Proof Theory
%J Science of Computer Progamming (SCP)
%V 22
%N 3
%P 197-230
%I Elsevier North-Holland, Inc
%C Amsterdam, The Netherlands, The Netherlands
%X 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
%U http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein1994d.pdf
%U http://dx.doi.org/10.1016/0167-6423(94)00004-2
%D 1994
%K dyntyp